![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > prid1 | Structured version Visualization version Unicode version |
Description: An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 24-Jun-1993.) |
Ref | Expression |
---|---|
prid1.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
prid1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prid1.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | prid1g 4069 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
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 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 |
This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-v 3033 df-un 3395 df-sn 3960 df-pr 3962 |
This theorem is referenced by: prid2 4072 prnz 4082 preqr1OLD 4140 preq12b 4142 prel12 4143 unisn2 4532 opi1 4669 opeluu 4671 dmrnssfld 5099 funopg 5621 fveqf1o 6218 2dom 7660 opthreg 8141 dfac2 8579 brdom7disj 8977 brdom6disj 8978 reelprrecn 9649 pnfxr 11435 m1expcl2 12332 hash2prb 12674 sadcf 14506 prmreclem2 14940 xpsfrnel2 15549 setcepi 16061 grpss 16765 efgi0 17448 vrgpf 17496 vrgpinv 17497 frgpuptinv 17499 frgpup2 17504 frgpnabllem1 17587 dmdprdpr 17760 dprdpr 17761 cnmsgnsubg 19222 m2detleiblem5 19727 m2detleiblem3 19731 m2detleiblem4 19732 m2detleib 19733 indistopon 20093 indiscld 20184 xpstopnlem1 20901 xpstopnlem2 20903 xpsdsval 21474 i1f1lem 22726 i1f1 22727 dvnfre 22985 c1lip2 23029 aannenlem2 23364 cxplogb 23802 ppiublem2 24210 lgsdir2lem3 24332 eengbas 25090 ebtwntg 25091 wlkntrl 25371 usgra2wlkspthlem2 25427 constr3lem4 25454 usg2wlkonot 25690 usg2wotspth 25691 eupath 25788 psgnid 28684 prsiga 29027 coinflippvt 29390 subfacp1lem3 29977 kur14lem7 30007 fprb 30484 noxp1o 30624 nobnddown 30661 onint1 31180 poimirlem22 32026 pw2f1ocnv 35963 fvrcllb0d 36356 fvrcllb0da 36357 corclrcl 36370 relexp0idm 36378 corcltrcl 36402 refsum2cnlem1 37421 fourierdlem103 38185 fourierdlem104 38186 prsal 38291 1wlk2v2e 40045 eulerpathpr 40152 zlmodzxzscm 40646 zlmodzxzldeplem3 40803 |
Copyright terms: Public domain | W3C validator |