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

Theorem rexeqbidv 2909
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 2903 . 2  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  B  ps )
)
3 raleqbidv.2 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
43rexbidv 2718 . 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 1652   E.wrex 2698
This theorem is referenced by:  supeq123d  7447  fpwwe2lem13  8509  vdwpc  13340  ramval  13368  mreexexlemd  13861  iscat  13889  iscatd  13890  catidex  13891  ismnd  14684  mndpropd  14713  gsumval2a  14774  isgrp  14808  isgrpd2e  14819  cayleyth  15105  iscyg  15481  ltbval  16524  opsrval  16527  neiptopnei  17188  is1stc  17496  2ndc1stc  17506  2ndcsep  17514  islly  17523  isnlly  17524  ucnval  18299  imasdsf1olem  18395  met2ndc  18545  evthicc  19348  nb3graprlem2  21453  isplig  21757  isgrp2d  21815  isgrpda  21877  isexid  21897  isrngo  21958  isrngod  21959  nmoofval  22255  iscvm  24938  cvmlift2lem13  24994  br8  25371  br6  25372  br4  25373  brsegle  26034  hilbert1.1  26080  cover2g  26407  mzpcompact2lem  26799  eldioph  26807  aomclem8  27127  psgnfval  27391  2wlksot  28287  2spthsot  28288  frgra2v  28326  lshpset  29713  cvrfval  30003  isatl  30034  ishlat1  30087  llnset  30239  lplnset  30263  lvolset  30306  lineset  30472  lcfl7N  32236  lcfrlem8  32284  lcfrlem9  32285  lcf1o  32286  hvmapffval  32493  hvmapfval  32494  hvmapval  32495
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rex 2703
  Copyright terms: Public domain W3C validator