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

Theorem rexeqbi1dv 3041
Description: Equality deduction for restricted existential quantifier. (Contributed by NM, 18-Mar-1997.)
Hypothesis
Ref Expression
raleqd.1  |-  ( A  =  B  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
rexeqbi1dv  |-  ( A  =  B  ->  ( E. x  e.  A  ph  <->  E. x  e.  B  ps ) )
Distinct variable groups:    x, A    x, B
Allowed substitution hints:    ph( x)    ps( x)

Proof of Theorem rexeqbi1dv
StepHypRef Expression
1 rexeq 3033 . 2  |-  ( A  =  B  ->  ( E. x  e.  A  ph  <->  E. x  e.  B  ph ) )
2 raleqd.1 . . 3  |-  ( A  =  B  ->  ( ph 
<->  ps ) )
32rexbidv 2946 . 2  |-  ( A  =  B  ->  ( E. x  e.  B  ph  <->  E. x  e.  B  ps ) )
41, 3bitrd 256 1  |-  ( A  =  B  ->  ( E. x  e.  A  ph  <->  E. x  e.  B  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437   E.wrex 2783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rex 2788
This theorem is referenced by:  fri  4816  frsn  4925  isofrlem  6246  f1oweALT  6791  frxp  6917  1sdom  7781  oieq2  8028  zfregcl  8109  ishaus  20269  isreg  20279  isnrm  20282  lebnumlem3  21887  1vwmgra  25576  3vfriswmgra  25578  isgrpo  25769  isexid2  25898  ismndo2  25918  rngomndo  25994  pjhth  26881  bnj1154  29596  frmin  30267  stoweidlem28  37457
  Copyright terms: Public domain W3C validator