![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > tpex | Structured version Visualization version Unicode version |
Description: An unordered triple of classes exists. (Contributed by NM, 10-Apr-1994.) |
Ref | Expression |
---|---|
tpex |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-tp 3973 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | prex 4642 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | snex 4641 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | unex 6589 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | eqeltri 2525 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pr 4639 ax-un 6583 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-rex 2743 df-v 3047 df-dif 3407 df-un 3409 df-nul 3732 df-sn 3969 df-pr 3971 df-tp 3973 df-uni 4199 |
This theorem is referenced by: fr3nr 6606 en3lp 8121 prdsval 15353 imasval 15411 imasvalOLD 15412 fnfuc 15850 fucval 15863 setcval 15972 catcval 15991 estrcval 16009 estrreslem1 16022 estrres 16024 fnxpc 16061 xpcval 16062 symgval 17020 psrval 18586 xrsex 18983 om1val 22061 wlkntrl 25292 constr2trl 25329 constr2spth 25330 constr2pth 25331 2pthon 25332 2pthon3v 25334 usgra2adedgwlkon 25343 usg2wlk 25345 usg2wlkon 25346 constr3lem1 25373 constr3cyclpe 25391 3v3e3cycl2 25392 signswbase 29443 signswplusg 29444 ldualset 32691 erngset 34367 erngset-rN 34375 dvaset 34572 dvhset 34649 hlhilset 35505 rabren3dioph 35658 mendval 36049 rngcvalALTV 40016 ringcvalALTV 40062 lmod1zrnlvec 40340 |
Copyright terms: Public domain | W3C validator |