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  4316  preq12b  4318  prel12  4319  unisn2  4717  opi1  4858  opeluu  4860  dmrnssfld  5292  funopg  5822  fveqf1o  6435  2dom  7893  opthreg  8376  dfac2  8814  brdom7disj  9212  brdom6disj  9213  reelprrecn  9885  pnfxr  11784  m1expcl2  12702  hash2prb  13066  sadcf  14962  prmreclem2  15408  xpsfrnel2  15997  setcepi  16510  grpss  17212  efgi0  17905  vrgpf  17953  vrgpinv  17954  frgpuptinv  17956  frgpup2  17961  frgpnabllem1  18048  dmdprdpr  18220  dprdpr  18221  cnmsgnsubg  19690  m2detleiblem5  20198  m2detleiblem3  20202  m2detleiblem4  20203  m2detleib  20204  indistopon  20563  indiscld  20653  xpstopnlem1  21370  xpstopnlem2  21372  xpsdsval  21944  i1f1lem  23207  i1f1  23208  dvnfre  23466  c1lip2  23510  aannenlem2  23833  cxplogb  24269  ppiublem2  24673  lgsdir2lem3  24797  eengbas  25607  ebtwntg  25608  wlkntrl  25886  usgra2wlkspthlem2  25942  constr3lem4  25969  usg2wlkonot  26204  usg2wotspth  26205  eupath  26302  psgnid  28972  prsiga  29315  coinflippvt  29667  subfacp1lem3  30212  kur14lem7  30242  fprb  30710  noxp1o  30857  nobnddown  30894  onint1  31412  poimirlem22  32395  pw2f1ocnv  36416  fvrcllb0d  36798  fvrcllb0da  36799  corclrcl  36812  relexp0idm  36820  corcltrcl  36844  refsum2cnlem1  38013  fourierdlem103  38896  fourierdlem104  38897  prsal  39008  usgr2trlncl  40958  umgrwwlks2on  41153  1wlk2v2e  41316  eulerpathpr  41400  zlmodzxzscm  41920  zlmodzxzldeplem3  42077