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

Theorem rexeqbi1dv 3067
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 3059 . 2  |-  ( A  =  B  ->  ( E. x  e.  A  ph  <->  E. x  e.  B  ph ) )
2 raleqd.1 . . 3  |-  ( A  =  B  ->  ( ph 
<->  ps ) )
32rexbidv 2973 . 2  |-  ( A  =  B  ->  ( E. x  e.  B  ph  <->  E. x  e.  B  ps ) )
41, 3bitrd 253 1  |-  ( A  =  B  ->  ( E. x  e.  A  ph  <->  E. x  e.  B  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1379   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820
This theorem is referenced by:  fri  4841  frsn  5070  isofrlem  6224  f1oweALT  6768  frxp  6893  1sdom  7722  oieq2  7938  zfregcl  8020  ishaus  19617  isreg  19627  isnrm  19630  lebnumlem3  21226  1vwmgra  24707  3vfriswmgra  24709  isgrpo  24902  isexid2  25031  ismndo2  25051  rngomndo  25127  pjhth  26015  frmin  28927  stoweidlem28  31356  bnj1154  33152
  Copyright terms: Public domain W3C validator