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 4239 | . 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ {𝐴, 𝐵}) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐴 ∈ {𝐴, 𝐵} |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 1977 Vcvv 3173 {cpr 4127 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-un 3545 df-sn 4126 df-pr 4128 |
This theorem is referenced by: prid2 4242 prnz 4253 preqr1OLD 4320 preq12b 4322 prel12 4323 unisn2 4722 opi1 4864 opeluu 4866 dmrnssfld 5305 funopg 5836 fveqf1o 6457 2dom 7915 opthreg 8398 dfac2 8836 brdom7disj 9234 brdom6disj 9235 reelprrecn 9907 pnfxr 9971 m1expcl2 12744 hash2prb 13111 sadcf 15013 prmreclem2 15459 xpsfrnel2 16048 setcepi 16561 grpss 17263 efgi0 17956 vrgpf 18004 vrgpinv 18005 frgpuptinv 18007 frgpup2 18012 frgpnabllem1 18099 dmdprdpr 18271 dprdpr 18272 cnmsgnsubg 19742 m2detleiblem5 20250 m2detleiblem3 20254 m2detleiblem4 20255 m2detleib 20256 indistopon 20615 indiscld 20705 xpstopnlem1 21422 xpstopnlem2 21424 xpsdsval 21996 i1f1lem 23262 i1f1 23263 dvnfre 23521 c1lip2 23565 aannenlem2 23888 cxplogb 24324 ppiublem2 24728 lgsdir2lem3 24852 eengbas 25661 ebtwntg 25662 wlkntrl 26092 usgra2wlkspthlem2 26148 constr3lem4 26175 usg2wlkonot 26410 usg2wotspth 26411 eupath 26508 psgnid 29178 prsiga 29521 coinflippvt 29873 subfacp1lem3 30418 kur14lem7 30448 fprb 30916 noxp1o 31063 nobnddown 31100 onint1 31618 poimirlem22 32601 pw2f1ocnv 36622 fvrcllb0d 37004 fvrcllb0da 37005 corclrcl 37018 relexp0idm 37026 corcltrcl 37050 refsum2cnlem1 38219 fourierdlem103 39102 fourierdlem104 39103 prsal 39214 usgr2trlncl 40966 umgrwwlks2on 41161 1wlk2v2e 41324 eulerpathpr 41408 zlmodzxzscm 41928 zlmodzxzldeplem3 42085 |
Copyright terms: Public domain | W3C validator |