Theorem prid1 3735

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

Syntax hints:   e. wcel 1688   _Vcvv 2789   {cpr 3642

This theorem is referenced by:  prid2  3736  prnz  3746  preqr1  3787  preq12b  3789  prel12  3790  opi1  4239  unisn2  4521  opeluu  4525  dmrnssfld  4937  funopg  5252  fveqf1o  5767  2dom  6928  opthreg  7314  dfac2  7752  brdom7disj  8151  brdom6disj  8152  pnfxr  10450  m1expcl2  11119  sadcf  12638  prmreclem2  12958  xpsfrnel2  13461  setcepi  13914  grpss  14497  efgi0  15023  vrgpf  15071  vrgpinv  15072  frgpuptinv  15074  frgpup2  15079  frgpnabllem1  15155  dmdprdpr  15278  dprdpr  15279  indistopon  16732  indiscld  16822  xpstopnlem1  17494  xpstopnlem2  17496  xpsdsval  17939  i1f1lem  19038  i1f1  19039  dvf  19251  dvnfre  19295  dvmptcj  19311  dvmptre  19312  dvmptim  19313  rolle  19331  cmvth  19332  mvth  19333  dvlip  19334  dvlipcn  19335  c1lip2  19339  dvle  19348  dvivthlem1  19349  dvivth  19351  lhop2  19356  dvcnvre  19360  dvfsumle  19362  dvfsumge  19363  dvfsumabs  19364  dvfsumlem2  19368  dvfsum2  19375  ftc2  19385  itgparts  19388  itgsubstlem  19389  aannenlem2  19703  aalioulem3  19708  taylthlem2  19747  taylth  19748  efcvx  19819  pige3  19879  dvrelog  19978  advlog  19995  advlogexp  19996  logccv  20004  dvcxp1  20076  loglesqr  20092  divsqrsumlem  20268  ppiublem2  20436  logexprlim  20458  lgsdir2lem3  20558  logdivsum  20676  log2sumbnd  20687  subfacp1lem3  23117  kur14lem7  23147  eupath  23309  fprb  23530  noxp1o  23720  axfelem10  23756  onint1  24295  toplat  24689  pfsubkl  25446  pw2f1ocnv  26529  cnmsgnsubg  26833  lhe4.4ex1a  26945  refsum2cnlem1  27107  dvcosre  27140  itgsin0pilem1  27143  itgsinexplem1  27147

This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265

This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-un 3158  df-sn 3647  df-pr 3648