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

Theorem rexeqbidv 2749
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.)
Hypotheses
Ref Expression
raleqbidv.1  |-  ( ph  ->  A  =  B )
raleqbidv.2  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
rexeqbidv  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  B  ch )
)
Distinct variable groups:    x, A    x, B    ph, x
Allowed substitution hints:    ps( x)    ch( x)

Proof of Theorem rexeqbidv
StepHypRef Expression
1 raleqbidv.1 . . 3  |-  ( ph  ->  A  =  B )
21rexeqdv 2743 . 2  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  B  ps )
)
3 raleqbidv.2 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
43rexbidv 2564 . 2  |-  ( ph  ->  ( E. x  e.  B  ps  <->  E. x  e.  B  ch )
)
52, 4bitrd 244 1  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623   E.wrex 2544
This theorem is referenced by:  fpwwe2lem13  8264  vdwpc  13027  ramval  13055  mreexexlemd  13546  iscat  13574  iscatd  13575  catidex  13576  ismnd  14369  mndpropd  14398  gsumval2a  14459  isgrp  14493  isgrpd2e  14504  cayleyth  14790  iscyg  15166  ltbval  16213  opsrval  16216  is1stc  17167  2ndc1stc  17177  2ndcsep  17185  islly  17194  isnlly  17195  imasdsf1olem  17937  met2ndc  18069  evthicc  18819  isplig  20844  isgrp2d  20902  isgrpda  20964  isexid  20984  isrngo  21045  isrngod  21046  nmoofval  21340  iscvm  23790  cvmlift2lem13  23846  br8  24113  br6  24114  br4  24115  brsegle  24731  hilbert1.1  24777  isdir2  25292  dffprod  25319  cnegvex2b  25662  rnegvex2b  25663  isiso  25825  isfuna  25834  bisig0  26062  cover2g  26359  mzpcompact2lem  26829  eldioph  26837  supeq123d  27158  aomclem8  27159  psgnfval  27423  frgra2v  28177  1vwmgra  28181  3vfriswmgra  28183  lshpset  29168  cvrfval  29458  isatl  29489  ishlat1  29542  llnset  29694  lplnset  29718  lvolset  29761  lineset  29927  lcfl7N  31691  lcfrlem8  31739  lcfrlem9  31740  lcf1o  31741  hvmapffval  31948  hvmapfval  31949  hvmapval  31950
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-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549
  Copyright terms: Public domain W3C validator