Theorem prid1 4718

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

Syntax hints:   ∈ wcel 2141  Vcvv 3453  {cpr 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3907  df-sn 4580  df-pr 4582

This theorem is referenced by:  prid2  4719  prnz  4733  preq12b  4805  unisn2  5259  opi1  5433  opeluu  5435  dmrnssfld  5946  funopg  6549  fprb  7172  fveqf1o  7280  2dom  9004  dif1en  9123  opthreg  9566  djuss  9871  dfac2b  10080  brdom7disj  10481  brdom6disj  10482  reelprrecn  11158  0elpr01  11167  pnfxr  11229  m1expcl2  14091  hash2prb  14478  sadcf  16477  prmreclem2  16943  fnpr2ob  17578  setcepi  18111  setc2obas  18117  setc2ohom  18118  cat1  18120  grpss  18986  efgi0  19750  vrgpf  19798  vrgpinv  19799  frgpuptinv  19801  frgpup2  19806  frgpnabllem1  19903  dmdprdpr  20081  dprdpr  20082  cnmsgnsubg  21616  m2detleiblem5  22672  m2detleiblem3  22676  m2detleiblem4  22677  m2detleib  22678  indistopon  23048  indiscld  23138  xpstopnlem1  23856  xpstopnlem2  23858  xpsdsval  24428  ehl2eudis  25471  i1f1lem  25738  i1f1  25739  dvnfre  26001  c1lip2  26047  aannenlem2  26380  cxplogb  26838  ppiublem2  27254  lgsdir2lem3  27378  noxp1o  27714  noextendlt  27720  nosepdmlem  27734  nolt02o  27746  nosupbnd1lem5  27763  nosupbnd2lem1  27766  noinfno  27769  noinfbnd1  27780  noinfbnd2lem1  27781  noetasuplem1  27784  eengbas  29138  ebtwntg  29139  structvtxval  29178  usgr2trlncl  29916  usgrwwlks2on  30114  umgrwwlks2on  30115  wlk2v2e  30315  eulerpathpr  30398  s2rnOLD  33082  psgnid  33237  trsp2cyc  33263  cyc3fv1  33277  cnmsgn0g  33286  constr01  33999  constrss  34000  constrelextdg2  34004  nn0constr  34018  prsiga  34388  coinflippvt  34742  subfacp1lem3  35492  kur14lem7  35522  ex-sategoelel12  35737  onint1  36769  poimirlem22  38101  pw2f1ocnv  43574  2omomeqom  43840  omcl3g  43871  fvrcllb0d  44229  fvrcllb0da  44230  corclrcl  44243  relexp0idm  44251  corcltrcl  44275  mnuprdlem1  44808  mnuprdlem3  44810  mnurndlem1  44817  nregmodellem  45552  refsum2cnlem1  45577  limsup10exlem  46306  fourierdlem103  46743  fourierdlem104  46744  prsal  46852  usgrgrtrirex  48532  stgr1  48543  stgrnbgr0  48546  grlimgrtrilem1  48583  gpgiedgdmellem  48628  gpgvtx0  48635  gpgprismgr4cycllem3  48679  gpgprismgr4cycllem9  48685  zlmodzxzscm  48939  zlmodzxzldeplem3  49084  2arympt  49231  rrx2pxel  49293  rrx2linesl  49325  2sphere0  49332  setc1onsubc  50183