Theorem prid1 4329

Description: An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 24-Jun-1993.)

Hypothesis

Ref	Expression
prid1.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
prid1	⊢ 𝐴 ∈ {𝐴, 𝐵}

Proof of Theorem prid1

Step	Hyp	Ref	Expression
1		prid1.1	. 2 ⊢ 𝐴 ∈ V
2		prid1g 4327	. 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ {𝐴, 𝐵})
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ {𝐴, 𝐵}

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