Theorem prid1 4716

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

Syntax hints:   ∈ wcel 2109  Vcvv 3438  {cpr 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-sn 4580  df-pr 4582

This theorem is referenced by:  prid2  4717  prnz  4731  preq12b  4804  unisn2  5254  opi1  5415  opeluu  5417  dmrnssfld  5919  funopg  6520  fprb  7134  fveqf1o  7243  2dom  8962  dif1en  9084  dif1enOLD  9086  opthreg  9533  djuss  9835  dfac2b  10044  brdom7disj  10444  brdom6disj  10445  reelprrecn  11120  pnfxr  11188  m1expcl2  14010  hash2prb  14397  sadcf  16382  prmreclem2  16847  fnpr2ob  17480  setcepi  18013  setc2obas  18019  setc2ohom  18020  cat1  18022  grpss  18851  efgi0  19617  vrgpf  19665  vrgpinv  19666  frgpuptinv  19668  frgpup2  19673  frgpnabllem1  19770  dmdprdpr  19948  dprdpr  19949  cnmsgnsubg  21502  m2detleiblem5  22528  m2detleiblem3  22532  m2detleiblem4  22533  m2detleib  22534  indistopon  22904  indiscld  22994  xpstopnlem1  23712  xpstopnlem2  23714  xpsdsval  24285  ehl2eudis  25338  i1f1lem  25606  i1f1  25607  dvnfre  25872  c1lip2  25919  aannenlem2  26253  cxplogb  26712  ppiublem2  27130  lgsdir2lem3  27254  noxp1o  27591  noextendlt  27597  nosepdmlem  27611  nolt02o  27623  nosupbnd1lem5  27640  nosupbnd2lem1  27643  noinfno  27646  noinfbnd1  27657  noinfbnd2lem1  27658  noetasuplem1  27661  eengbas  28944  ebtwntg  28945  structvtxval  28984  usgr2trlncl  29723  umgrwwlks2on  29920  wlk2v2e  30119  eulerpathpr  30202  s2rnOLD  32898  psgnid  33052  trsp2cyc  33078  cyc3fv1  33092  cnmsgn0g  33101  constr01  33711  constrss  33712  constrconj  33714  constrelextdg2  33716  nn0constr  33730  prsiga  34100  coinflippvt  34455  subfacp1lem3  35157  kur14lem7  35187  ex-sategoelel12  35402  onint1  36425  poimirlem22  37624  pw2f1ocnv  43013  2omomeqom  43279  omcl3g  43310  fvrcllb0d  43669  fvrcllb0da  43670  corclrcl  43683  relexp0idm  43691  corcltrcl  43715  mnuprdlem1  44248  mnuprdlem3  44250  mnurndlem1  44257  nregmodellem  44993  refsum2cnlem1  45018  limsup10exlem  45757  fourierdlem103  46194  fourierdlem104  46195  prsal  46303  usgrgrtrirex  47938  stgr1  47949  stgrnbgr0  47952  grlimgrtrilem1  47989  gpgiedgdmellem  48034  gpgvtx0  48041  gpgprismgr4cycllem3  48085  gpgprismgr4cycllem9  48091  zlmodzxzscm  48345  zlmodzxzldeplem3  48491  2arympt  48638  rrx2pxel  48700  rrx2linesl  48732  2sphere0  48739  setc1onsubc  49591