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

Theorem prid1 3872
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 3870 . 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 1721   _Vcvv 2916   {cpr 3775
This theorem is referenced by:  prid2  3873  prnz  3883  preqr1  3932  preq12b  3934  prel12  3935  opi1  4390  unisn2  4670  opeluu  4674  dmrnssfld  5088  funopg  5444  fveqf1o  5988  2dom  7138  opthreg  7529  dfac2  7967  brdom7disj  8365  brdom6disj  8366  pnfxr  10669  m1expcl2  11358  sadcf  12920  prmreclem2  13240  xpsfrnel2  13745  setcepi  14198  grpss  14781  efgi0  15307  vrgpf  15355  vrgpinv  15356  frgpuptinv  15358  frgpup2  15363  frgpnabllem1  15439  dmdprdpr  15562  dprdpr  15563  indistopon  17020  indiscld  17110  xpstopnlem1  17794  xpstopnlem2  17796  xpsdsval  18364  i1f1lem  19534  i1f1  19535  dvf  19747  dvnfre  19791  dvmptcj  19807  dvmptre  19808  dvmptim  19809  rolle  19827  cmvth  19828  mvth  19829  dvlip  19830  dvlipcn  19831  c1lip2  19835  dvle  19844  dvivthlem1  19845  dvivth  19847  lhop2  19852  dvcnvre  19856  dvfsumle  19858  dvfsumge  19859  dvfsumabs  19860  dvfsumlem2  19864  dvfsum2  19871  ftc2  19881  itgparts  19884  itgsubstlem  19885  aannenlem2  20199  aalioulem3  20204  taylthlem2  20243  taylth  20244  efcvx  20318  pige3  20378  dvrelog  20481  advlog  20498  advlogexp  20499  logccv  20507  dvcxp1  20579  loglesqr  20595  divsqrsumlem  20771  ppiublem2  20940  logexprlim  20962  lgsdir2lem3  21062  logdivsum  21180  log2sumbnd  21191  wlkntrl  21515  constr3lem4  21587  eupath  21656  prsiga  24467  coinflippvt  24695  lgamgulmlem2  24767  subfacp1lem3  24821  kur14lem7  24851  fprb  25343  noxp1o  25534  nobnddown  25569  onint1  26103  dvreasin  26179  dvreacos  26180  areacirclem2  26181  areacirclem3  26182  pw2f1ocnv  26998  cnmsgnsubg  27302  lhe4.4ex1a  27414  refsum2cnlem1  27575  dvcosre  27608  itgsin0pilem1  27611  itgsinexplem1  27615  usgra2wlkspthlem2  28037  usg2wlkonot  28080  usg2wotspth  28081
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 2385
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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-un 3285  df-sn 3780  df-pr 3781
  Copyright terms: Public domain W3C validator