Theorem prid1 4742

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

Syntax hints:   ∈ wcel 2107  Vcvv 3463  {cpr 4608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3465  df-un 3936  df-sn 4607  df-pr 4609

This theorem is referenced by:  prid2  4743  prnz  4757  preq12b  4830  unisn2  5292  opi1  5453  opeluu  5455  dmrnssfld  5964  funopg  6580  fprb  7196  fveqf1o  7304  2dom  9052  dif1en  9182  dif1enOLD  9184  opthreg  9640  djuss  9942  dfac2b  10153  brdom7disj  10553  brdom6disj  10554  reelprrecn  11229  pnfxr  11297  m1expcl2  14108  hash2prb  14493  sadcf  16472  prmreclem2  16937  fnpr2ob  17574  setcepi  18104  setc2obas  18110  setc2ohom  18111  cat1  18113  grpss  18941  efgi0  19706  vrgpf  19754  vrgpinv  19755  frgpuptinv  19757  frgpup2  19762  frgpnabllem1  19859  dmdprdpr  20037  dprdpr  20038  cnmsgnsubg  21549  m2detleiblem5  22579  m2detleiblem3  22583  m2detleiblem4  22584  m2detleib  22585  indistopon  22955  indiscld  23045  xpstopnlem1  23763  xpstopnlem2  23765  xpsdsval  24336  ehl2eudis  25392  i1f1lem  25660  i1f1  25661  dvnfre  25926  c1lip2  25973  aannenlem2  26307  cxplogb  26765  ppiublem2  27183  lgsdir2lem3  27307  noxp1o  27644  noextendlt  27650  nosepdmlem  27664  nolt02o  27676  nosupbnd1lem5  27693  nosupbnd2lem1  27696  noinfno  27699  noinfbnd1  27710  noinfbnd2lem1  27711  noetasuplem1  27714  eengbas  28926  ebtwntg  28927  structvtxval  28966  usgr2trlncl  29708  umgrwwlks2on  29905  wlk2v2e  30104  eulerpathpr  30187  s2rnOLD  32868  psgnid  33056  trsp2cyc  33082  cyc3fv1  33096  cnmsgn0g  33105  constr01  33722  constrss  33723  constrconj  33725  constrelextdg2  33727  nn0constr  33741  prsiga  34091  coinflippvt  34446  subfacp1lem3  35146  kur14lem7  35176  ex-sategoelel12  35391  onint1  36409  poimirlem22  37608  pw2f1ocnv  43012  2omomeqom  43278  omcl3g  43309  fvrcllb0d  43668  fvrcllb0da  43669  corclrcl  43682  relexp0idm  43690  corcltrcl  43714  mnuprdlem1  44248  mnuprdlem3  44250  mnurndlem1  44257  refsum2cnlem1  44999  limsup10exlem  45744  fourierdlem103  46181  fourierdlem104  46182  prsal  46290  usgrgrtrirex  47875  stgr1  47886  stgrnbgr0  47889  grlimgrtrilem1  47919  gpgedgel  47965  gpgvtx0  47966  zlmodzxzscm  48231  zlmodzxzldeplem3  48377  2arympt  48528  rrx2pxel  48590  rrx2linesl  48622  2sphere0  48629