Theorem prid1 4004

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 4002	. 2 |- ( A e. _V -> A e. { A , B } )
3	1, 2	ax-mp 5	1 |- A e. { A , B }

Syntax hints:   e. wcel 1756   _Vcvv 2993   {cpr 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995  df-un 3354  df-sn 3899  df-pr 3901

This theorem is referenced by:  prid2  4005  prnz  4015  preqr1  4067  preq12b  4069  prel12  4070  unisn2  4449  opi1  4580  opeluu  4582  dmrnssfld  5119  funopg  5471  fveqf1o  6021  2dom  7403  opthreg  7845  dfac2  8321  brdom7disj  8719  brdom6disj  8720  reelprrecn  9395  pnfxr  11113  m1expcl2  11908  hash2prd  12202  sadcf  13670  prmreclem2  13999  xpsfrnel2  14524  setcepi  14977  grpss  15580  efgi0  16238  vrgpf  16286  vrgpinv  16287  frgpuptinv  16289  frgpup2  16294  frgpnabllem1  16372  dmdprdpr  16570  dprdpr  16571  cnmsgnsubg  18029  m2detleiblem5  18453  m2detleiblem3  18457  m2detleiblem4  18458  m2detleib  18459  indistopon  18627  indiscld  18717  xpstopnlem1  19404  xpstopnlem2  19406  xpsdsval  19978  i1f1lem  21189  i1f1  21190  dvnfre  21448  c1lip2  21492  aannenlem2  21817  ppiublem2  22564  lgsdir2lem3  22686  eengbas  23249  ebtwntg  23250  wlkntrl  23483  constr3lem4  23555  eupath  23624  prsiga  26596  coinflippvt  26889  subfacp1lem3  27092  kur14lem7  27122  fprb  27606  noxp1o  27829  nobnddown  27864  onint1  28317  pw2f1ocnv  29412  refsum2cnlem1  29785  hash2prv  30252  hash2sspr  30253  usgra2wlkspthlem2  30323  usg2wlkonot  30428  usg2wotspth  30429  zlmodzxzscm  30783  zlmodzxzldeplem3  31041