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

Theorem rabbidva 2792
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 2639 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  <->  ch ) )
3 rabbi 2731 . 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 1632    e. wcel 1696   A.wral 2556   {crab 2560
This theorem is referenced by:  rabbidv  2793  rabeqbidva  2797  rabbi2dva  3390  ordintdif  4457  rabxfrd  4571  onsucmin  4628  seinxp  4772  dfinfmr  9747  ixxin  10689  incexc2  12313  smueqlem  12697  gcdass  12740  pcneg  12942  ramval  13071  acsfn  13577  monpropd  13656  submod  14896  odngen  14904  sylow3lem6  14959  efgsfo  15064  rrgsupp  16048  coe1mul2lem2  16361  mretopd  16845  ordtbaslem  16934  ordtrest  16948  ordtrest2lem  16949  leordtval  16959  xkopt  17365  xkoco1cn  17367  xkoco2cn  17368  xkoinjcn  17397  r0cld  17445  stdbdbl  18079  minveclem3b  18808  minveclem4  18812  lhop1lem  19376  mumul  20435  sqff1o  20436  lgsquadlem1  20609  lgsquadlem2  20610  grpoidinv2  20901  grpoinv  20910  xppreima  23226  cnvordtrestixx  23312  vdgrun  23908  lineunray  24842  lineelsb2  24843  linecom  24845  ee7.2aOLD  24972  itg2addnclem2  25004  itgaddnclem2  25010  iblabsnclem  25014  svs2  25590  svs3  25591  supexr  25734  xsyysx  26248  istopclsd  26878  diophren  26999  rabrenfdioph  27000  dsmmbas2  27306  dsmmacl  27310  frlmbas  27326  frlmsslss2  27348  pwfi2f1o  27363  f1omvdcnv  27490  pmtrmvd  27501  acsfn1p  27610  idomrootle  27614  idomodle  27615  hausgraph  27634  lfl1dim2N  29934  pmapat  30574  pmapglbx  30580  dvhb1dimN  31797  dia0  31864  mapdval2N  32442  mapdsn  32453  hlhilocv  32772
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-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-ral 2561  df-rab 2565
  Copyright terms: Public domain W3C validator