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

Theorem rabbidva 2813
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 2660 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  <->  ch ) )
3 rabbi 2752 . 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 1633    e. wcel 1701   A.wral 2577   {crab 2581
This theorem is referenced by:  rabbidv  2814  rabeqbidva  2818  rabbi2dva  3411  ordintdif  4478  rabxfrd  4592  onsucmin  4649  seinxp  4793  dfinfmr  9776  ixxin  10720  incexc2  12344  smueqlem  12728  gcdass  12771  pcneg  12973  ramval  13102  acsfn  13610  monpropd  13689  submod  14929  odngen  14937  sylow3lem6  14992  efgsfo  15097  rrgsupp  16081  coe1mul2lem2  16394  mretopd  16885  ordtbaslem  16974  ordtrest  16988  ordtrest2lem  16989  leordtval  16999  xkopt  17405  xkoco1cn  17407  xkoco2cn  17408  xkoinjcn  17437  r0cld  17485  stdbdbl  18115  minveclem3b  18845  minveclem4  18849  lhop1lem  19413  mumul  20472  sqff1o  20473  lgsquadlem1  20646  lgsquadlem2  20647  grpoidinv2  20938  grpoinv  20947  xppreima  23208  cnvordtrestixx  23380  vdgrun  24177  lineunray  25156  lineelsb2  25157  linecom  25159  ee7.2aOLD  25286  itg2addnclem2  25318  itgaddnclem2  25324  iblabsnclem  25328  istopclsd  25923  diophren  26044  rabrenfdioph  26045  dsmmbas2  26351  dsmmacl  26355  frlmbas  26371  frlmsslss2  26393  pwfi2f1o  26408  f1omvdcnv  26535  pmtrmvd  26546  acsfn1p  26655  idomrootle  26659  idomodle  26660  hausgraph  26679  vdgreun  27569  frisusgranb  27589  lfl1dim2N  29130  pmapat  29770  pmapglbx  29776  dvhb1dimN  30993  dia0  31060  mapdval2N  31638  mapdsn  31649  hlhilocv  31968
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-ral 2582  df-rab 2586
  Copyright terms: Public domain W3C validator