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  vdgrun  23304  lineunray  24181  lineelsb2  24182  linecom  24184  ee7.2aOLD  24311  svs2  24899  svs3  24900  supexr  25043  xsyysx  25557  istopclsd  26187  diophren  26308  rabrenfdioph  26309  dsmmbas2  26615  dsmmacl  26619  frlmbas  26635  frlmsslss2  26657  pwfi2f1o  26672  f1omvdcnv  26799  pmtrmvd  26810  acsfn1p  26919  idomrootle  26923  idomodle  26924  hausgraph  26943  lfl1dim2N  28685  pmapat  29325  pmapglbx  29331  dvhb1dimN  30548  dia0  30615  mapdval2N  31193  mapdsn  31204  hlhilocv  31523
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