Theorem prid1 4071

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	|- A e. _V

Assertion

Ref	Expression
prid1	|- A e. { A , B }

Proof of Theorem prid1

Step	Hyp	Ref	Expression
1		prid1.1	. 2 |- A e. _V
2		prid1g 4069	. 2 |- ( A e. _V -> A e. { A , B } )
3	1, 2	ax-mp 5	1 |- A e. { A , B }

Syntax hints:   e. wcel 1904   _Vcvv 3031   {cpr 3961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-un 3395  df-sn 3960  df-pr 3962

This theorem is referenced by:  prid2  4072  prnz  4082  preqr1OLD  4140  preq12b  4142  prel12  4143  unisn2  4532  opi1  4669  opeluu  4671  dmrnssfld  5099  funopg  5621  fveqf1o  6218  2dom  7660  opthreg  8141  dfac2  8579  brdom7disj  8977  brdom6disj  8978  reelprrecn  9649  pnfxr  11435  m1expcl2  12332  hash2prb  12674  sadcf  14506  prmreclem2  14940  xpsfrnel2  15549  setcepi  16061  grpss  16765  efgi0  17448  vrgpf  17496  vrgpinv  17497  frgpuptinv  17499  frgpup2  17504  frgpnabllem1  17587  dmdprdpr  17760  dprdpr  17761  cnmsgnsubg  19222  m2detleiblem5  19727  m2detleiblem3  19731  m2detleiblem4  19732  m2detleib  19733  indistopon  20093  indiscld  20184  xpstopnlem1  20901  xpstopnlem2  20903  xpsdsval  21474  i1f1lem  22726  i1f1  22727  dvnfre  22985  c1lip2  23029  aannenlem2  23364  cxplogb  23802  ppiublem2  24210  lgsdir2lem3  24332  eengbas  25090  ebtwntg  25091  wlkntrl  25371  usgra2wlkspthlem2  25427  constr3lem4  25454  usg2wlkonot  25690  usg2wotspth  25691  eupath  25788  psgnid  28684  prsiga  29027  coinflippvt  29390  subfacp1lem3  29977  kur14lem7  30007  fprb  30484  noxp1o  30624  nobnddown  30661  onint1  31180  poimirlem22  32026  pw2f1ocnv  35963  fvrcllb0d  36356  fvrcllb0da  36357  corclrcl  36370  relexp0idm  36378  corcltrcl  36402  refsum2cnlem1  37421  fourierdlem103  38185  fourierdlem104  38186  prsal  38291  1wlk2v2e  40045  eulerpathpr  40152  zlmodzxzscm  40646  zlmodzxzldeplem3  40803