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

Theorem rexeqbidv 2861
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 2855 . 2  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  B  ps )
)
3 raleqbidv.2 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
43rexbidv 2671 . 2  |-  ( ph  ->  ( E. x  e.  B  ps  <->  E. x  e.  B  ch )
)
52, 4bitrd 245 1  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649   E.wrex 2651
This theorem is referenced by:  fpwwe2lem13  8451  vdwpc  13276  ramval  13304  mreexexlemd  13797  iscat  13825  iscatd  13826  catidex  13827  ismnd  14620  mndpropd  14649  gsumval2a  14710  isgrp  14744  isgrpd2e  14755  cayleyth  15041  iscyg  15417  ltbval  16460  opsrval  16463  neiptopnei  17120  is1stc  17426  2ndc1stc  17436  2ndcsep  17444  islly  17453  isnlly  17454  ucnval  18229  imasdsf1olem  18312  met2ndc  18444  evthicc  19224  nb3graprlem2  21328  isplig  21614  isgrp2d  21672  isgrpda  21734  isexid  21754  isrngo  21815  isrngod  21816  nmoofval  22112  iscvm  24726  cvmlift2lem13  24782  br8  25138  br6  25139  br4  25140  brsegle  25757  hilbert1.1  25803  cover2g  26108  mzpcompact2lem  26500  eldioph  26508  supeq123d  26828  aomclem8  26829  psgnfval  27093  frgra2v  27753  lshpset  29094  cvrfval  29384  isatl  29415  ishlat1  29468  llnset  29620  lplnset  29644  lvolset  29687  lineset  29853  lcfl7N  31617  lcfrlem8  31665  lcfrlem9  31666  lcf1o  31667  hvmapffval  31874  hvmapfval  31875  hvmapval  31876
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2381  df-clel 2384  df-nfc 2513  df-rex 2656
  Copyright terms: Public domain W3C validator