Theorem prid1 4723

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  {cpr 4590

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  prid2  4724  prnz  4738  preq12b  4808  unisn2  5270  opi1  5442  opeluu  5444  dmrnssfld  5964  funopg  6597  fprb  7225  fveqf1o  7336  2dom  9089  dif1en  9208  opthreg  9649  djuss  10031  dfac2b  10239  brdom7disj  10640  brdom6disj  10641  reelprrecn  11322  0elpr01  11331  pnfxr  11393  m1expcl2  14258  hash2prb  14647  sadcf  16655  fnpr2ob  17762  setcepi  18295  setc2obas  18301  setc2ohom  18302  cat1  18304  degenmgm  19169  degenmgm2  19172  grpss  19197  efgi0  19967  vrgpf  20015  vrgpinv  20016  frgpuptinv  20018  frgpup2  20023  frgpnabllem1  20120  dmdprdpr  20298  dprdpr  20299  cnmsgnsubg  21916  m2detleiblem5  22973  m2detleiblem3  22977  m2detleiblem4  22978  m2detleib  22979  indistopon  23352  indiscld  23442  xpstopnlem1  24161  xpstopnlem2  24163  xpsdsval  24733  dvnfre  26305  c1lip2  26351  aannenlem2  26689  ppiublem2  27563  lgsdir2lem3  27687  noxp1o  28053  noextendlt  28059  nosepdmlem  28073  nolt02o  28085  nosupbnd1lem5  28102  nosupbnd2lem1  28105  noinfno  28108  noinfbnd1  28119  noinfbnd2lem1  28120  noetasuplem1  28123  eengbas  29592  ebtwntg  29593  structvtxval  29632  wlk2v2e  30791  eulerpathpr  30874  psgnid  33734  trsp2cyc  33760  cnmsgn0g  33783  prsiga  34846  coinflippvt  35200  subfacp1lem3  36127  kur14lem7  36157  ex-sategoelel12  36372  onint1  37428  poimirlem22  38765  pw2f1ocnv  44248  2omomeqom  44508  omcl3g  44539  relexp0idm  44918  corcltrcl  44942  mnuprdlem1  45459  mnuprdlem3  45461  mnurndlem1  45468  nregmodellem  46212  refsum2cnlem1  46270  fourierdlem103  47434  fourierdlem104  47435  prsal  47543  usgrgrtrirex  49263  stgrnbgr0  49277  grlimgrtrilem1  49314  zlmodzxzldeplem3  49829  setc1onsubc  50955  parswapprop  50992  par2hom  50994  par2diag  50995  fuconuniqlem  50996  fuconuniqvalslem  50998