![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > prid1 | Unicode version |
Description: An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
prid1.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
prid1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prid1.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | prid1g 3874 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 8 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem is referenced by: prid2 3877 prnz 3887 preqr1 3936 preq12b 3938 prel12 3939 opi1 4394 unisn2 4674 opeluu 4678 dmrnssfld 5092 funopg 5448 fveqf1o 5992 2dom 7142 opthreg 7533 dfac2 7971 brdom7disj 8369 brdom6disj 8370 pnfxr 10673 m1expcl2 11362 sadcf 12924 prmreclem2 13244 xpsfrnel2 13749 setcepi 14202 grpss 14785 efgi0 15311 vrgpf 15359 vrgpinv 15360 frgpuptinv 15362 frgpup2 15367 frgpnabllem1 15443 dmdprdpr 15566 dprdpr 15567 indistopon 17024 indiscld 17114 xpstopnlem1 17798 xpstopnlem2 17800 xpsdsval 18368 i1f1lem 19538 i1f1 19539 dvf 19751 dvnfre 19795 dvmptcj 19811 dvmptre 19812 dvmptim 19813 rolle 19831 cmvth 19832 mvth 19833 dvlip 19834 dvlipcn 19835 c1lip2 19839 dvle 19848 dvivthlem1 19849 dvivth 19851 lhop2 19856 dvcnvre 19860 dvfsumle 19862 dvfsumge 19863 dvfsumabs 19864 dvfsumlem2 19868 dvfsum2 19875 ftc2 19885 itgparts 19888 itgsubstlem 19889 aannenlem2 20203 aalioulem3 20208 taylthlem2 20247 taylth 20248 efcvx 20322 pige3 20382 dvrelog 20485 advlog 20502 advlogexp 20503 logccv 20511 dvcxp1 20583 loglesqr 20599 divsqrsumlem 20775 ppiublem2 20944 logexprlim 20966 lgsdir2lem3 21066 logdivsum 21184 log2sumbnd 21195 wlkntrl 21519 constr3lem4 21591 eupath 21660 prsiga 24471 coinflippvt 24699 lgamgulmlem2 24771 subfacp1lem3 24825 kur14lem7 24855 fprb 25347 noxp1o 25538 nobnddown 25573 onint1 26107 dvreasin 26183 dvreacos 26184 areacirclem2 26185 areacirclem3 26186 pw2f1ocnv 27002 cnmsgnsubg 27306 lhe4.4ex1a 27418 refsum2cnlem1 27579 dvcosre 27612 itgsin0pilem1 27615 itgsinexplem1 27619 usgra2wlkspthlem2 28041 usg2wlkonot 28084 usg2wotspth 28085 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2389 |
This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-clab 2395 df-cleq 2401 df-clel 2404 df-nfc 2533 df-v 2922 df-un 3289 df-sn 3784 df-pr 3785 |
Copyright terms: Public domain | W3C validator |