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

Theorem rabbidva 2779
Description: Equivalent wff's yield equal restricted class abstractions (deduction rule). (Contributed by NM, 28-Nov-2003.)
Hypothesis
Ref Expression
rabbidva.1  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
Assertion
Ref Expression
rabbidva  |-  ( ph  ->  { x  e.  A  |  ps }  =  {
x  e.  A  |  ch } )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem rabbidva
StepHypRef Expression
1 rabbidva.1 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
21ralrimiva 2626 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  <->  ch ) )
3 rabbi 2718 . 2  |-  ( A. x  e.  A  ( ps 
<->  ch )  <->  { x  e.  A  |  ps }  =  { x  e.  A  |  ch } )
42, 3sylib 188 1  |-  ( ph  ->  { x  e.  A  |  ps }  =  {
x  e.  A  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1623    e. wcel 1684   A.wral 2543   {crab 2547
This theorem is referenced by:  rabbidv  2780  rabeqbidva  2784  rabbi2dva  3377  ordintdif  4441  rabxfrd  4555  onsucmin  4612  seinxp  4756  dfinfmr  9731  ixxin  10673  incexc2  12297  smueqlem  12681  gcdass  12724  pcneg  12926  ramval  13055  acsfn  13561  monpropd  13640  submod  14880  odngen  14888  sylow3lem6  14943  efgsfo  15048  rrgsupp  16032  coe1mul2lem2  16345  mretopd  16829  ordtbaslem  16918  ordtrest  16932  ordtrest2lem  16933  leordtval  16943  xkopt  17349  xkoco1cn  17351  xkoco2cn  17352  xkoinjcn  17381  r0cld  17429  stdbdbl  18063  minveclem3b  18792  minveclem4  18796  lhop1lem  19360  mumul  20419  sqff1o  20420  lgsquadlem1  20593  lgsquadlem2  20594  grpoidinv2  20885  grpoinv  20894  xppreima  23211  cnvordtrestixx  23297  vdgrun  23893  lineunray  24770  lineelsb2  24771  linecom  24773  ee7.2aOLD  24900  svs2  25487  svs3  25488  supexr  25631  xsyysx  26145  istopclsd  26775  diophren  26896  rabrenfdioph  26897  dsmmbas2  27203  dsmmacl  27207  frlmbas  27223  frlmsslss2  27245  pwfi2f1o  27260  f1omvdcnv  27387  pmtrmvd  27398  acsfn1p  27507  idomrootle  27511  idomodle  27512  hausgraph  27531  lfl1dim2N  29312  pmapat  29952  pmapglbx  29958  dvhb1dimN  31175  dia0  31242  mapdval2N  31820  mapdsn  31831  hlhilocv  32150
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-ral 2548  df-rab 2552
  Copyright terms: Public domain W3C validator