Theorem prid1 4052

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

Syntax hints:   e. wcel 1826   _Vcvv 3034   {cpr 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-un 3394  df-sn 3945  df-pr 3947

This theorem is referenced by:  prid2  4053  prnz  4063  preqr1  4118  preq12b  4120  prel12  4121  unisn2  4501  opi1  4629  opeluu  4631  dmrnssfld  5174  funopg  5528  fveqf1o  6106  2dom  7507  opthreg  7949  dfac2  8424  brdom7disj  8822  brdom6disj  8823  reelprrecn  9495  pnfxr  11242  m1expcl2  12091  hash2prd  12422  hash2prv  12429  hash2sspr  12430  sadcf  14105  prmreclem2  14437  xpsfrnel2  14972  setcepi  15484  grpss  16188  efgi0  16855  vrgpf  16903  vrgpinv  16904  frgpuptinv  16906  frgpup2  16911  frgpnabllem1  16994  dmdprdpr  17211  dprdpr  17212  cnmsgnsubg  18704  m2detleiblem5  19212  m2detleiblem3  19216  m2detleiblem4  19217  m2detleib  19218  indistopon  19587  indiscld  19678  xpstopnlem1  20395  xpstopnlem2  20397  xpsdsval  20969  i1f1lem  22181  i1f1  22182  dvnfre  22440  c1lip2  22484  aannenlem2  22810  cxplogb  23244  ppiublem2  23595  lgsdir2lem3  23717  eengbas  24405  ebtwntg  24406  wlkntrl  24685  usgra2wlkspthlem2  24741  constr3lem4  24768  usg2wlkonot  25004  usg2wotspth  25005  eupath  25102  prsiga  28280  coinflippvt  28606  subfacp1lem3  28815  kur14lem7  28845  fprb  29368  noxp1o  29591  nobnddown  29626  onint1  30067  pw2f1ocnv  31145  refsum2cnlem1  31579  fourierdlem103  32158  fourierdlem104  32159  zlmodzxzscm  33146  zlmodzxzldeplem3  33303  relexp0idm  38238  corclrcl  38248  corcltrcl  38249