Theorem prid1 4719

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4151  df-sn 4585  df-pr 4587

This theorem is used by:  prid2  4720  prnz  4734  preq12b  4804  unisn2  5265  opi1  5436  opeluu  5438  dmrnssfld  5955  funopg  6575  fprb  7200  fveqf1o  7311  2dom  9062  dif1en  9181  opthreg  9623  djuss  10005  dfac2b  10213  brdom7disj  10614  brdom6disj  10615  reelprrecn  11296  0elpr01  11305  pnfxr  11367  m1expcl2  14232  hash2prb  14621  sadcf  16629  fnpr2ob  17736  setcepi  18269  setc2obas  18275  setc2ohom  18276  cat1  18278  degenmgm  19143  degenmgm2  19146  grpss  19171  efgi0  19940  vrgpf  19988  vrgpinv  19989  frgpuptinv  19991  frgpup2  19996  frgpnabllem1  20093  dmdprdpr  20271  dprdpr  20272  cnmsgnsubg  21889  m2detleiblem5  22946  m2detleiblem3  22950  m2detleiblem4  22951  m2detleib  22952  indistopon  23325  indiscld  23415  xpstopnlem1  24134  xpstopnlem2  24136  xpsdsval  24706  dvnfre  26278  c1lip2  26324  aannenlem2  26662  ppiublem2  27536  lgsdir2lem3  27660  noxp1o  28026  noextendlt  28032  nosepdmlem  28046  nolt02o  28058  nosupbnd1lem5  28075  nosupbnd2lem1  28078  noinfno  28081  noinfbnd1  28092  noinfbnd2lem1  28093  noetasuplem1  28096  eengbas  29565  ebtwntg  29566  structvtxval  29605  wlk2v2e  30764  eulerpathpr  30847  psgnid  33705  trsp2cyc  33731  cnmsgn0g  33754  prsiga  34810  coinflippvt  35164  subfacp1lem3  36034  kur14lem7  36064  ex-sategoelel12  36279  onint1  37330  poimirlem22  38654  pw2f1ocnv  44138  2omomeqom  44399  omcl3g  44430  relexp0idm  44809  corcltrcl  44833  mnuprdlem1  45350  mnuprdlem3  45352  mnurndlem1  45359  nregmodellem  46100  refsum2cnlem1  46148  fourierdlem103  47313  fourierdlem104  47314  prsal  47422  usgrgrtrirex  49142  stgrnbgr0  49156  grlimgrtrilem1  49193  zlmodzxzldeplem3  49708  setc1onsubc  50834  parswapprop  50871  par2hom  50873  par2diag  50874  fuconuniqlem  50875  fuconuniqvalslem  50877