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 4295 | . 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ {𝐴, 𝐵}) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐴 ∈ {𝐴, 𝐵} |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 1990 Vcvv 3200 {cpr 4179 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-un 3579 df-sn 4178 df-pr 4180 |
This theorem is referenced by: prid2 4298 prnz 4310 preqr1OLD 4380 preq12b 4382 prel12 4383 unisn2 4794 opi1 4937 opeluu 4939 dmrnssfld 5384 funopg 5922 fveqf1o 6557 2dom 8029 opthreg 8515 dfac2 8953 brdom7disj 9353 brdom6disj 9354 reelprrecn 10028 pnfxr 10092 m1expcl2 12882 hash2prb 13254 sadcf 15175 prmreclem2 15621 xpsfrnel2 16225 setcepi 16738 grpss 17440 efgi0 18133 vrgpf 18181 vrgpinv 18182 frgpuptinv 18184 frgpup2 18189 frgpnabllem1 18276 dmdprdpr 18448 dprdpr 18449 cnmsgnsubg 19923 m2detleiblem5 20431 m2detleiblem3 20435 m2detleiblem4 20436 m2detleib 20437 indistopon 20805 indiscld 20895 xpstopnlem1 21612 xpstopnlem2 21614 xpsdsval 22186 i1f1lem 23456 i1f1 23457 dvnfre 23715 c1lip2 23761 aannenlem2 24084 cxplogb 24524 ppiublem2 24928 lgsdir2lem3 25052 eengbas 25861 ebtwntg 25862 structvtxval 25910 usgr2trlncl 26656 umgrwwlks2on 26850 wlk2v2e 27017 eulerpathpr 27100 psgnid 29847 prsiga 30194 coinflippvt 30546 subfacp1lem3 31164 kur14lem7 31194 fprb 31669 noxp1o 31816 noextendlt 31822 nosepdmlem 31833 nolt02o 31845 nosupbnd1lem5 31858 nosupbnd2lem1 31861 noetalem1 31863 onint1 32448 poimirlem22 33431 pw2f1ocnv 37604 fvrcllb0d 37985 fvrcllb0da 37986 corclrcl 37999 relexp0idm 38007 corcltrcl 38031 refsum2cnlem1 39196 limsup10exlem 40004 fourierdlem103 40426 fourierdlem104 40427 prsal 40538 zlmodzxzscm 42135 zlmodzxzldeplem3 42291 |
Copyright terms: Public domain | W3C validator |