Theorem prid1 4678

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

Syntax hints:   ∈ wcel 2110  Vcvv 3408  {cpr 4543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-un 3871  df-sn 4542  df-pr 4544

This theorem is referenced by:  prid2  4679  prnz  4693  preq12b  4761  unisn2  5205  opi1  5352  opeluu  5354  dmrnssfld  5839  funopg  6414  fprb  7009  fveqf1o  7113  2dom  8707  dif1en  8840  opthreg  9233  djuss  9536  dfac2b  9744  brdom7disj  10145  brdom6disj  10146  reelprrecn  10821  pnfxr  10887  m1expcl2  13657  hash2prb  14038  sadcf  16012  prmreclem2  16470  fnpr2ob  17063  setcepi  17594  setc2obas  17600  setc2ohom  17601  cat1  17603  grpss  18385  efgi0  19110  vrgpf  19158  vrgpinv  19159  frgpuptinv  19161  frgpup2  19166  frgpnabllem1  19258  dmdprdpr  19436  dprdpr  19437  cnmsgnsubg  20539  m2detleiblem5  21522  m2detleiblem3  21526  m2detleiblem4  21527  m2detleib  21528  indistopon  21898  indiscld  21988  xpstopnlem1  22706  xpstopnlem2  22708  xpsdsval  23279  ehl2eudis  24319  i1f1lem  24586  i1f1  24587  dvnfre  24849  c1lip2  24895  aannenlem2  25222  cxplogb  25669  ppiublem2  26084  lgsdir2lem3  26208  eengbas  27072  ebtwntg  27073  structvtxval  27112  usgr2trlncl  27847  umgrwwlks2on  28041  wlk2v2e  28240  eulerpathpr  28323  s2rn  30938  psgnid  31083  trsp2cyc  31109  cyc3fv1  31123  cnmsgn0g  31132  prsiga  31811  coinflippvt  32163  subfacp1lem3  32857  kur14lem7  32887  ex-sategoelel12  33102  noxp1o  33603  noextendlt  33609  nosepdmlem  33623  nolt02o  33635  nosupbnd1lem5  33652  nosupbnd2lem1  33655  noinfno  33658  noinfbnd1  33669  noinfbnd2lem1  33670  noetasuplem1  33673  onint1  34375  poimirlem22  35536  pw2f1ocnv  40562  fvrcllb0d  40978  fvrcllb0da  40979  corclrcl  40992  relexp0idm  41000  corcltrcl  41024  mnuprdlem1  41563  mnuprdlem3  41565  mnurndlem1  41572  refsum2cnlem1  42253  limsup10exlem  42988  fourierdlem103  43425  fourierdlem104  43426  prsal  43534  zlmodzxzscm  45366  zlmodzxzldeplem3  45516  2arympt  45668  rrx2pxel  45730  rrx2linesl  45762  2sphere0  45769