MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prid1 Unicode version

Theorem prid1 3747
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
StepHypRef Expression
1 prid1.1 . 2  |-  A  e. 
_V
2 prid1g 3745 . 2  |-  ( A  e.  _V  ->  A  e.  { A ,  B } )
31, 2ax-mp 8 1  |-  A  e. 
{ A ,  B }
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   _Vcvv 2801   {cpr 3654
This theorem is referenced by:  prid2  3748  prnz  3758  preqr1  3802  preq12b  3804  prel12  3805  opi1  4256  unisn2  4538  opeluu  4542  dmrnssfld  4954  funopg  5302  fveqf1o  5822  2dom  6949  opthreg  7335  dfac2  7773  brdom7disj  8172  brdom6disj  8173  pnfxr  10471  m1expcl2  11141  sadcf  12660  prmreclem2  12980  xpsfrnel2  13483  setcepi  13936  grpss  14519  efgi0  15045  vrgpf  15093  vrgpinv  15094  frgpuptinv  15096  frgpup2  15101  frgpnabllem1  15177  dmdprdpr  15300  dprdpr  15301  indistopon  16754  indiscld  16844  xpstopnlem1  17516  xpstopnlem2  17518  xpsdsval  17961  i1f1lem  19060  i1f1  19061  dvf  19273  dvnfre  19317  dvmptcj  19333  dvmptre  19334  dvmptim  19335  rolle  19353  cmvth  19354  mvth  19355  dvlip  19356  dvlipcn  19357  c1lip2  19361  dvle  19370  dvivthlem1  19371  dvivth  19373  lhop2  19378  dvcnvre  19382  dvfsumle  19384  dvfsumge  19385  dvfsumabs  19386  dvfsumlem2  19390  dvfsum2  19397  ftc2  19407  itgparts  19410  itgsubstlem  19411  aannenlem2  19725  aalioulem3  19730  taylthlem2  19769  taylth  19770  efcvx  19841  pige3  19901  dvrelog  20000  advlog  20017  advlogexp  20018  logccv  20026  dvcxp1  20098  loglesqr  20114  divsqrsumlem  20290  ppiublem2  20458  logexprlim  20480  lgsdir2lem3  20580  logdivsum  20698  log2sumbnd  20709  prsiga  23507  coinflippvt  23700  subfacp1lem3  23728  kur14lem7  23758  eupath  23920  fprb  24200  noxp1o  24391  nobnddown  24426  onint1  24960  dvreasin  25026  dvreacos  25027  areacirclem2  25028  areacirclem3  25029  toplat  25393  pfsubkl  26150  pw2f1ocnv  27233  cnmsgnsubg  27537  lhe4.4ex1a  27649  refsum2cnlem1  27811  dvcosre  27844  itgsin0pilem1  27847  itgsinexplem1  27851  constr3lem4  28393
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170  df-sn 3659  df-pr 3660
  Copyright terms: Public domain W3C validator