MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexeqbidv 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:  fpwwe2lem13  8506  vdwpc  13336  ramval  13364  mreexexlemd  13857  iscat  13885  iscatd  13886  catidex  13887  ismnd  14680  mndpropd  14709  gsumval2a  14770  isgrp  14804  isgrpd2e  14815  cayleyth  15101  iscyg  15477  ltbval  16520  opsrval  16523  neiptopnei  17184  is1stc  17492  2ndc1stc  17502  2ndcsep  17510  islly  17519  isnlly  17520  ucnval  18295  imasdsf1olem  18391  met2ndc  18541  evthicc  19344  nb3graprlem2  21449  isplig  21753  isgrp2d  21811  isgrpda  21873  isexid  21893  isrngo  21954  isrngod  21955  nmoofval  22251  iscvm  24934  cvmlift2lem13  24990  br8  25368  br6  25369  br4  25370  brsegle  25990  hilbert1.1  26036  cover2g  26353  mzpcompact2lem  26745  eldioph  26753  supeq123d  27073  aomclem8  27074  psgnfval  27338  2wlksot  28208  2spthsot  28209  frgra2v  28247  lshpset  29615  cvrfval  29905  isatl  29936  ishlat1  29989  llnset  30141  lplnset  30165  lvolset  30208  lineset  30374  lcfl7N  32138  lcfrlem8  32186  lcfrlem9  32187  lcf1o  32188  hvmapffval  32395  hvmapfval  32396  hvmapval  32397
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