Theorem prid1 3876

Description: An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-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 3874	. 2 |- ( A e. _V -> A e. { A , B } )
3	1, 2	ax-mp 8	1 |- A e. { A , B }

Syntax hints:   e. wcel 1721   _Vcvv 2920   {cpr 3779

This theorem is referenced by:  prid2  3877  prnz  3887  preqr1  3936  preq12b  3938  prel12  3939  opi1  4394  unisn2  4674  opeluu  4678  dmrnssfld  5092  funopg  5448  fveqf1o  5992  2dom  7142  opthreg  7533  dfac2  7971  brdom7disj  8369  brdom6disj  8370  pnfxr  10673  m1expcl2  11362  sadcf  12924  prmreclem2  13244  xpsfrnel2  13749  setcepi  14202  grpss  14785  efgi0  15311  vrgpf  15359  vrgpinv  15360  frgpuptinv  15362  frgpup2  15367  frgpnabllem1  15443  dmdprdpr  15566  dprdpr  15567  indistopon  17024  indiscld  17114  xpstopnlem1  17798  xpstopnlem2  17800  xpsdsval  18368  i1f1lem  19538  i1f1  19539  dvf  19751  dvnfre  19795  dvmptcj  19811  dvmptre  19812  dvmptim  19813  rolle  19831  cmvth  19832  mvth  19833  dvlip  19834  dvlipcn  19835  c1lip2  19839  dvle  19848  dvivthlem1  19849  dvivth  19851  lhop2  19856  dvcnvre  19860  dvfsumle  19862  dvfsumge  19863  dvfsumabs  19864  dvfsumlem2  19868  dvfsum2  19875  ftc2  19885  itgparts  19888  itgsubstlem  19889  aannenlem2  20203  aalioulem3  20208  taylthlem2  20247  taylth  20248  efcvx  20322  pige3  20382  dvrelog  20485  advlog  20502  advlogexp  20503  logccv  20511  dvcxp1  20583  loglesqr  20599  divsqrsumlem  20775  ppiublem2  20944  logexprlim  20966  lgsdir2lem3  21066  logdivsum  21184  log2sumbnd  21195  wlkntrl  21519  constr3lem4  21591  eupath  21660  prsiga  24471  coinflippvt  24699  lgamgulmlem2  24771  subfacp1lem3  24825  kur14lem7  24855  fprb  25347  noxp1o  25538  nobnddown  25573  onint1  26107  dvreasin  26183  dvreacos  26184  areacirclem2  26185  areacirclem3  26186  pw2f1ocnv  27002  cnmsgnsubg  27306  lhe4.4ex1a  27418  refsum2cnlem1  27579  dvcosre  27612  itgsin0pilem1  27615  itgsinexplem1  27619  usgra2wlkspthlem2  28041  usg2wlkonot  28084  usg2wotspth  28085

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-v 2922  df-un 3289  df-sn 3784  df-pr 3785