Theorem prid1 4698

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

Syntax hints:   ∈ wcel 2106  Vcvv 3432  {cpr 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-sn 4562  df-pr 4564

This theorem is referenced by:  prid2  4699  prnz  4713  preq12b  4781  unisn2  5236  opi1  5383  opeluu  5385  dmrnssfld  5879  funopg  6468  fprb  7069  fveqf1o  7175  2dom  8820  dif1en  8945  opthreg  9376  djuss  9678  dfac2b  9886  brdom7disj  10287  brdom6disj  10288  reelprrecn  10963  pnfxr  11029  m1expcl2  13804  hash2prb  14186  sadcf  16160  prmreclem2  16618  fnpr2ob  17269  setcepi  17803  setc2obas  17809  setc2ohom  17810  cat1  17812  grpss  18597  efgi0  19326  vrgpf  19374  vrgpinv  19375  frgpuptinv  19377  frgpup2  19382  frgpnabllem1  19474  dmdprdpr  19652  dprdpr  19653  cnmsgnsubg  20782  m2detleiblem5  21774  m2detleiblem3  21778  m2detleiblem4  21779  m2detleib  21780  indistopon  22151  indiscld  22242  xpstopnlem1  22960  xpstopnlem2  22962  xpsdsval  23534  ehl2eudis  24586  i1f1lem  24853  i1f1  24854  dvnfre  25116  c1lip2  25162  aannenlem2  25489  cxplogb  25936  ppiublem2  26351  lgsdir2lem3  26475  eengbas  27349  ebtwntg  27350  structvtxval  27391  usgr2trlncl  28128  umgrwwlks2on  28322  wlk2v2e  28521  eulerpathpr  28604  s2rn  31218  psgnid  31364  trsp2cyc  31390  cyc3fv1  31404  cnmsgn0g  31413  prsiga  32099  coinflippvt  32451  subfacp1lem3  33144  kur14lem7  33174  ex-sategoelel12  33389  noxp1o  33866  noextendlt  33872  nosepdmlem  33886  nolt02o  33898  nosupbnd1lem5  33915  nosupbnd2lem1  33918  noinfno  33921  noinfbnd1  33932  noinfbnd2lem1  33933  noetasuplem1  33936  onint1  34638  poimirlem22  35799  pw2f1ocnv  40859  fvrcllb0d  41301  fvrcllb0da  41302  corclrcl  41315  relexp0idm  41323  corcltrcl  41347  mnuprdlem1  41890  mnuprdlem3  41892  mnurndlem1  41899  refsum2cnlem1  42580  limsup10exlem  43313  fourierdlem103  43750  fourierdlem104  43751  prsal  43859  zlmodzxzscm  45693  zlmodzxzldeplem3  45843  2arympt  45995  rrx2pxel  46057  rrx2linesl  46089  2sphere0  46096