Theorem prid1 4726

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3453  {cpr 4589

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-sn 4588  df-pr 4590

This theorem is used by:  prid2  4727  prnz  4741  preq12b  4813  unisn2  5273  opi1  5448  opeluu  5450  dmrnssfld  5962  funopg  6571  fprb  7196  fveqf1o  7307  2dom  9041  dif1en  9160  opthreg  9601  djuss  9929  dfac2b  10137  brdom7disj  10538  brdom6disj  10539  reelprrecn  11220  0elpr01  11229  pnfxr  11291  m1expcl2  14153  hash2prb  14541  sadcf  16549  fnpr2ob  17650  setcepi  18183  setc2obas  18189  setc2ohom  18190  cat1  18192  degenmgm  19056  degenmgm2  19059  grpss  19084  efgi0  19853  vrgpf  19901  vrgpinv  19902  frgpuptinv  19904  frgpup2  19909  frgpnabllem1  20006  dmdprdpr  20184  dprdpr  20185  cnmsgnsubg  21796  m2detleiblem5  22853  m2detleiblem3  22857  m2detleiblem4  22858  m2detleib  22859  indistopon  23232  indiscld  23322  xpstopnlem1  24041  xpstopnlem2  24043  xpsdsval  24613  ehl2eudis  25656  dvnfre  26186  c1lip2  26232  aannenlem2  26572  ppiublem2  27447  lgsdir2lem3  27571  noxp1o  27907  noextendlt  27913  nosepdmlem  27927  nolt02o  27939  nosupbnd1lem5  27956  nosupbnd2lem1  27959  noinfno  27962  noinfbnd1  27973  noinfbnd2lem1  27974  noetasuplem1  27977  eengbas  29446  ebtwntg  29447  structvtxval  29486  wlk2v2e  30645  eulerpathpr  30728  psgnid  33545  trsp2cyc  33571  cnmsgn0g  33594  prsiga  34649  coinflippvt  35004  subfacp1lem3  35769  kur14lem7  35799  ex-sategoelel12  36014  onint1  37076  poimirlem22  38399  pw2f1ocnv  43886  2omomeqom  44152  omcl3g  44183  relexp0idm  44563  corcltrcl  44587  mnuprdlem1  45104  mnuprdlem3  45106  mnurndlem1  45113  nregmodellem  45847  refsum2cnlem1  45879  fourierdlem103  47045  fourierdlem104  47046  prsal  47154  usgrgrtrirex  48874  stgrnbgr0  48888  grlimgrtrilem1  48925  zlmodzxzldeplem3  49440  rrx2pxel  49649  rrx2linesl  49681  2sphere0  49688  setc1onsubc  50536