Theorem prid1 4241

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

Syntax hints:   ∈ wcel 1977  Vcvv 3173  {cpr 4127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-sn 4126  df-pr 4128

This theorem is referenced by:  prid2  4242  prnz  4253  preqr1OLD  4320  preq12b  4322  prel12  4323  unisn2  4722  opi1  4864  opeluu  4866  dmrnssfld  5305  funopg  5836  fveqf1o  6457  2dom  7915  opthreg  8398  dfac2  8836  brdom7disj  9234  brdom6disj  9235  reelprrecn  9907  pnfxr  9971  m1expcl2  12744  hash2prb  13111  sadcf  15013  prmreclem2  15459  xpsfrnel2  16048  setcepi  16561  grpss  17263  efgi0  17956  vrgpf  18004  vrgpinv  18005  frgpuptinv  18007  frgpup2  18012  frgpnabllem1  18099  dmdprdpr  18271  dprdpr  18272  cnmsgnsubg  19742  m2detleiblem5  20250  m2detleiblem3  20254  m2detleiblem4  20255  m2detleib  20256  indistopon  20615  indiscld  20705  xpstopnlem1  21422  xpstopnlem2  21424  xpsdsval  21996  i1f1lem  23262  i1f1  23263  dvnfre  23521  c1lip2  23565  aannenlem2  23888  cxplogb  24324  ppiublem2  24728  lgsdir2lem3  24852  eengbas  25661  ebtwntg  25662  wlkntrl  26092  usgra2wlkspthlem2  26148  constr3lem4  26175  usg2wlkonot  26410  usg2wotspth  26411  eupath  26508  psgnid  29178  prsiga  29521  coinflippvt  29873  subfacp1lem3  30418  kur14lem7  30448  fprb  30916  noxp1o  31063  nobnddown  31100  onint1  31618  poimirlem22  32601  pw2f1ocnv  36622  fvrcllb0d  37004  fvrcllb0da  37005  corclrcl  37018  relexp0idm  37026  corcltrcl  37050  refsum2cnlem1  38219  fourierdlem103  39102  fourierdlem104  39103  prsal  39214  usgr2trlncl  40966  umgrwwlks2on  41161  1wlk2v2e  41324  eulerpathpr  41408  zlmodzxzscm  41928  zlmodzxzldeplem3  42085