Theorem prid1 4452

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

Syntax hints:   ∈ wcel 2155  Vcvv 3350  {cpr 4336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-un 3737  df-sn 4335  df-pr 4337

This theorem is referenced by:  prid2  4453  prnz  4464  preq12b  4533  prel12OLD  4534  unisn2  4955  opi1  5092  opeluu  5094  dmrnssfld  5553  funopg  6102  fveqf1o  6749  2dom  8233  opthreg  8728  opthregOLD  8730  djuss  8997  dfac2b  9204  dfac2OLD  9206  brdom7disj  9606  brdom6disj  9607  reelprrecn  10281  pnfxr  10346  m1expcl2  13089  hash2prb  13455  sadcf  15456  prmreclem2  15900  xpsfrnel2  16491  setcepi  17003  grpss  17707  efgi0  18397  vrgpf  18447  vrgpinv  18448  frgpuptinv  18450  frgpup2  18455  frgpnabllem1  18542  dmdprdpr  18715  dprdpr  18716  cnmsgnsubg  20195  m2detleiblem5  20708  m2detleiblem3  20712  m2detleiblem4  20713  m2detleib  20714  indistopon  21085  indiscld  21175  xpstopnlem1  21892  xpstopnlem2  21894  xpsdsval  22465  i1f1lem  23747  i1f1  23748  dvnfre  24006  c1lip2  24052  aannenlem2  24375  cxplogb  24815  ppiublem2  25219  lgsdir2lem3  25343  eengbas  26152  ebtwntg  26153  structvtxval  26190  usgr2trlncl  26948  umgrwwlks2on  27181  wlk2v2e  27435  eulerpathpr  27518  psgnid  30294  prsiga  30641  coinflippvt  30994  subfacp1lem3  31612  kur14lem7  31642  fprb  32114  noxp1o  32260  noextendlt  32266  nosepdmlem  32277  nolt02o  32289  nosupbnd1lem5  32302  nosupbnd2lem1  32305  noetalem1  32307  onint1  32887  poimirlem22  33855  pw2f1ocnv  38281  fvrcllb0d  38660  fvrcllb0da  38661  corclrcl  38674  relexp0idm  38682  corcltrcl  38706  refsum2cnlem1  39848  limsup10exlem  40642  fourierdlem103  41063  fourierdlem104  41064  prsal  41175  zlmodzxzscm  42804  zlmodzxzldeplem3  42960