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

Theorem prid1 3848
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 3846 . 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 1717   _Vcvv 2892   {cpr 3751
This theorem is referenced by:  prid2  3849  prnz  3859  preqr1  3907  preq12b  3909  prel12  3910  opi1  4364  unisn2  4644  opeluu  4648  dmrnssfld  5062  funopg  5418  fveqf1o  5961  2dom  7108  opthreg  7499  dfac2  7937  brdom7disj  8335  brdom6disj  8336  pnfxr  10638  m1expcl2  11323  sadcf  12885  prmreclem2  13205  xpsfrnel2  13710  setcepi  14163  grpss  14746  efgi0  15272  vrgpf  15320  vrgpinv  15321  frgpuptinv  15323  frgpup2  15328  frgpnabllem1  15404  dmdprdpr  15527  dprdpr  15528  indistopon  16981  indiscld  17071  xpstopnlem1  17755  xpstopnlem2  17757  xpsdsval  18312  i1f1lem  19441  i1f1  19442  dvf  19654  dvnfre  19698  dvmptcj  19714  dvmptre  19715  dvmptim  19716  rolle  19734  cmvth  19735  mvth  19736  dvlip  19737  dvlipcn  19738  c1lip2  19742  dvle  19751  dvivthlem1  19752  dvivth  19754  lhop2  19759  dvcnvre  19763  dvfsumle  19765  dvfsumge  19766  dvfsumabs  19767  dvfsumlem2  19771  dvfsum2  19778  ftc2  19788  itgparts  19791  itgsubstlem  19792  aannenlem2  20106  aalioulem3  20111  taylthlem2  20150  taylth  20151  efcvx  20225  pige3  20285  dvrelog  20388  advlog  20405  advlogexp  20406  logccv  20414  dvcxp1  20486  loglesqr  20502  divsqrsumlem  20678  ppiublem2  20847  logexprlim  20869  lgsdir2lem3  20969  logdivsum  21087  log2sumbnd  21098  constr3lem4  21475  eupath  21544  prsiga  24303  coinflippvt  24514  lgamgulmlem2  24586  subfacp1lem3  24640  kur14lem7  24670  fprb  25146  noxp1o  25337  nobnddown  25372  onint1  25906  dvreasin  25973  dvreacos  25974  areacirclem2  25975  areacirclem3  25976  pw2f1ocnv  26792  cnmsgnsubg  27096  lhe4.4ex1a  27208  refsum2cnlem1  27369  dvcosre  27402  itgsin0pilem1  27405  itgsinexplem1  27409
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
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 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-v 2894  df-un 3261  df-sn 3756  df-pr 3757
  Copyright terms: Public domain W3C validator