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

Theorem rabbidva 2949
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 2791 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  <->  ch ) )
3 rabbi 2888 . 2  |-  ( A. x  e.  A  ( ps 
<->  ch )  <->  { x  e.  A  |  ps }  =  { x  e.  A  |  ch } )
42, 3sylib 190 1  |-  ( ph  ->  { x  e.  A  |  ps }  =  {
x  e.  A  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653    e. wcel 1726   A.wral 2707   {crab 2711
This theorem is referenced by:  rabbidv  2950  rabeqbidva  2954  rabbi2dva  3551  ordintdif  4632  rabxfrd  4746  onsucmin  4803  seinxp  4946  dfinfmr  9987  ixxin  10935  incexc2  12620  smueqlem  13004  gcdass  13047  pcneg  13249  ramval  13378  acsfn  13886  monpropd  13965  submod  15205  odngen  15213  sylow3lem6  15268  efgsfo  15373  rrgsupp  16353  coe1mul2lem2  16663  mretopd  17158  ordtbaslem  17254  ordtrest  17268  ordtrest2lem  17269  leordtval  17279  xkopt  17689  xkoco1cn  17691  xkoco2cn  17692  xkoinjcn  17721  r0cld  17772  utopsnneiplem  18279  stdbdbl  18549  minveclem3b  19331  minveclem4  19335  lhop1lem  19899  mumul  20966  sqff1o  20967  lgsquadlem1  21140  lgsquadlem2  21141  vdgrun  21674  vdgrfiun  21675  grpoidinv2  21808  grpoinv  21817  xppreima  24061  cnvordtrestixx  24313  lineunray  26083  lineelsb2  26084  linecom  26086  ee7.2aOLD  26213  mbfposadd  26256  cnambfre  26257  itg2addnclem2  26259  iblabsnclem  26270  ftc1anclem1  26282  istopclsd  26756  diophren  26876  rabrenfdioph  26877  dsmmbas2  27182  dsmmacl  27186  frlmbas  27202  frlmsslss2  27224  pwfi2f1o  27239  f1omvdcnv  27366  pmtrmvd  27377  acsfn1p  27486  idomrootle  27490  idomodle  27491  hausgraph  27510  2pthwlkonot  28405  frisusgranb  28449  lfl1dim2N  29982  pmapat  30622  pmapglbx  30628  dvhb1dimN  31845  dia0  31912  mapdval2N  32490  mapdsn  32501  hlhilocv  32820
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-ral 2712  df-rab 2716
  Copyright terms: Public domain W3C validator