Theorem prid1 3694

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

Syntax hints:   e. wcel 1621   _Vcvv 2757   {cpr 3601

This theorem is referenced by:  prid2  3695  prnz  3705  preqr1  3746  preq12b  3748  prel12  3749  opi1  4198  unisn2  4480  opeluu  4484  dmrnssfld  4912  funopg  5211  fveqf1o  5726  2dom  6887  opthreg  7273  dfac2  7711  brdom7disj  8110  brdom6disj  8111  pnfxr  10408  m1expcl2  11077  sadcf  12592  prmreclem2  12912  xpsfrnel2  13415  setcepi  13868  grpss  14451  efgi0  14977  vrgpf  15025  vrgpinv  15026  frgpuptinv  15028  frgpup2  15033  frgpnabllem1  15109  dmdprdpr  15232  dprdpr  15233  indistopon  16686  indiscld  16776  xpstopnlem1  17448  xpstopnlem2  17450  xpsdsval  17893  i1f1lem  18992  i1f1  18993  dvf  19205  dvnfre  19249  dvmptcj  19265  dvmptre  19266  dvmptim  19267  rolle  19285  cmvth  19286  mvth  19287  dvlip  19288  dvlipcn  19289  c1lip2  19293  dvle  19302  dvivthlem1  19303  dvivth  19305  lhop2  19310  dvcnvre  19314  dvfsumle  19316  dvfsumge  19317  dvfsumabs  19318  dvfsumlem2  19322  dvfsum2  19329  ftc2  19339  itgparts  19342  itgsubstlem  19343  aannenlem2  19657  aalioulem3  19662  taylthlem2  19701  taylth  19702  efcvx  19773  pige3  19833  dvrelog  19932  advlog  19949  advlogexp  19950  logccv  19958  dvcxp1  20030  loglesqr  20046  divsqrsumlem  20222  ppiublem2  20390  logexprlim  20412  lgsdir2lem3  20512  logdivsum  20630  log2sumbnd  20641  subfacp1lem3  23071  kur14lem7  23101  eupath  23263  fprb  23484  noxp1o  23674  axfelem10  23710  onint1  24249  toplat  24643  pfsubkl  25400  pw2f1ocnv  26483  cnmsgnsubg  26787  lhe4.4ex1a  26899  refsum2cnlem1  27062

This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237

This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2759  df-un 3118  df-sn 3606  df-pr 3607