Theorem prid1 4707

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 4705	. 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ {𝐴, 𝐵})
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ {𝐴, 𝐵}

Syntax hints:   ∈ wcel 2114  Vcvv 3430  {cpr 4570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-sn 4569  df-pr 4571

This theorem is referenced by:  prid2  4708  prnz  4722  preq12b  4794  unisn2  5247  opi1  5416  opeluu  5418  dmrnssfld  5923  funopg  6526  fprb  7142  fveqf1o  7250  2dom  8970  dif1en  9089  opthreg  9530  djuss  9835  dfac2b  10044  brdom7disj  10444  brdom6disj  10445  reelprrecn  11121  pnfxr  11190  m1expcl2  14038  hash2prb  14425  sadcf  16413  prmreclem2  16879  fnpr2ob  17513  setcepi  18046  setc2obas  18052  setc2ohom  18053  cat1  18055  grpss  18921  efgi0  19686  vrgpf  19734  vrgpinv  19735  frgpuptinv  19737  frgpup2  19742  frgpnabllem1  19839  dmdprdpr  20017  dprdpr  20018  cnmsgnsubg  21567  m2detleiblem5  22600  m2detleiblem3  22604  m2detleiblem4  22605  m2detleib  22606  indistopon  22976  indiscld  23066  xpstopnlem1  23784  xpstopnlem2  23786  xpsdsval  24356  ehl2eudis  25399  i1f1lem  25666  i1f1  25667  dvnfre  25929  c1lip2  25975  aannenlem2  26306  cxplogb  26763  ppiublem2  27180  lgsdir2lem3  27304  noxp1o  27641  noextendlt  27647  nosepdmlem  27661  nolt02o  27673  nosupbnd1lem5  27690  nosupbnd2lem1  27693  noinfno  27696  noinfbnd1  27707  noinfbnd2lem1  27708  noetasuplem1  27711  eengbas  29064  ebtwntg  29065  structvtxval  29104  usgr2trlncl  29843  usgrwwlks2on  30041  umgrwwlks2on  30042  wlk2v2e  30242  eulerpathpr  30325  s2rnOLD  33019  psgnid  33173  trsp2cyc  33199  cyc3fv1  33213  cnmsgn0g  33222  constr01  33902  constrss  33903  constrconj  33905  constrelextdg2  33907  nn0constr  33921  prsiga  34291  coinflippvt  34645  subfacp1lem3  35380  kur14lem7  35410  ex-sategoelel12  35625  onint1  36647  poimirlem22  37977  pw2f1ocnv  43483  2omomeqom  43749  omcl3g  43780  fvrcllb0d  44138  fvrcllb0da  44139  corclrcl  44152  relexp0idm  44160  corcltrcl  44184  mnuprdlem1  44717  mnuprdlem3  44719  mnurndlem1  44726  nregmodellem  45461  refsum2cnlem1  45486  limsup10exlem  46218  fourierdlem103  46655  fourierdlem104  46656  prsal  46764  usgrgrtrirex  48438  stgr1  48449  stgrnbgr0  48452  grlimgrtrilem1  48489  gpgiedgdmellem  48534  gpgvtx0  48541  gpgprismgr4cycllem3  48585  gpgprismgr4cycllem9  48591  zlmodzxzscm  48845  zlmodzxzldeplem3  48990  2arympt  49137  rrx2pxel  49199  rrx2linesl  49231  2sphere0  49238  setc1onsubc  50089