![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > prid1 | Structured version Visualization version GIF 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 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
prid1 | ⊢ 𝐴 ∈ {𝐴, 𝐵} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prid1.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | prid1g 4327 | . 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ {𝐴, 𝐵}) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐴 ∈ {𝐴, 𝐵} |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2030 Vcvv 3231 {cpr 4212 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-v 3233 df-un 3612 df-sn 4211 df-pr 4213 |
This theorem is referenced by: prid2 4330 prnz 4341 preq12b 4413 prel12 4414 unisn2 4827 opi1 4966 opeluu 4968 dmrnssfld 5416 funopg 5960 fveqf1o 6597 2dom 8070 opthreg 8553 dfac2 8991 brdom7disj 9391 brdom6disj 9392 reelprrecn 10066 pnfxr 10130 m1expcl2 12922 hash2prb 13292 sadcf 15222 prmreclem2 15668 xpsfrnel2 16272 setcepi 16785 grpss 17487 efgi0 18179 vrgpf 18227 vrgpinv 18228 frgpuptinv 18230 frgpup2 18235 frgpnabllem1 18322 dmdprdpr 18494 dprdpr 18495 cnmsgnsubg 19971 m2detleiblem5 20479 m2detleiblem3 20483 m2detleiblem4 20484 m2detleib 20485 indistopon 20853 indiscld 20943 xpstopnlem1 21660 xpstopnlem2 21662 xpsdsval 22233 i1f1lem 23501 i1f1 23502 dvnfre 23760 c1lip2 23806 aannenlem2 24129 cxplogb 24569 ppiublem2 24973 lgsdir2lem3 25097 eengbas 25906 ebtwntg 25907 structvtxval 25955 usgr2trlncl 26712 umgrwwlks2on 26923 wlk2v2e 27135 eulerpathpr 27218 psgnid 29975 prsiga 30322 coinflippvt 30674 subfacp1lem3 31290 kur14lem7 31320 fprb 31795 noxp1o 31941 noextendlt 31947 nosepdmlem 31958 nolt02o 31970 nosupbnd1lem5 31983 nosupbnd2lem1 31986 noetalem1 31988 onint1 32573 poimirlem22 33561 pw2f1ocnv 37921 fvrcllb0d 38302 fvrcllb0da 38303 corclrcl 38316 relexp0idm 38324 corcltrcl 38348 refsum2cnlem1 39510 limsup10exlem 40322 fourierdlem103 40744 fourierdlem104 40745 prsal 40856 zlmodzxzscm 42460 zlmodzxzldeplem3 42616 |
Copyright terms: Public domain | W3C validator |