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

Theorem rexeqbidv 2923
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 2917 . 2  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  B  ps )
)
3 raleqbidv.2 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
43rexbidv 2732 . 2  |-  ( ph  ->  ( E. x  e.  B  ps  <->  E. x  e.  B  ch )
)
52, 4bitrd 246 1  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1653   E.wrex 2712
This theorem is referenced by:  supeq123d  7484  fpwwe2lem13  8548  vdwpc  13379  ramval  13407  mreexexlemd  13900  iscat  13928  iscatd  13929  catidex  13930  ismnd  14723  mndpropd  14752  gsumval2a  14813  isgrp  14847  isgrpd2e  14858  cayleyth  15144  iscyg  15520  ltbval  16563  opsrval  16566  neiptopnei  17227  is1stc  17535  2ndc1stc  17545  2ndcsep  17553  islly  17562  isnlly  17563  ucnval  18338  imasdsf1olem  18434  met2ndc  18584  evthicc  19387  nb3graprlem2  21492  isplig  21796  isgrp2d  21854  isgrpda  21916  isexid  21936  isrngo  21997  isrngod  21998  nmoofval  22294  iscvm  24977  cvmlift2lem13  25033  br8  25410  br6  25411  br4  25412  brsegle  26073  hilbert1.1  26119  cover2g  26454  mzpcompact2lem  26846  eldioph  26854  aomclem8  27174  psgnfval  27438  2wlksot  28423  2spthsot  28424  frgra2v  28487  lshpset  29874  cvrfval  30164  isatl  30195  ishlat1  30248  llnset  30400  lplnset  30424  lvolset  30467  lineset  30633  lcfl7N  32397  lcfrlem8  32445  lcfrlem9  32446  lcf1o  32447  hvmapffval  32654  hvmapfval  32655  hvmapval  32656
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-cleq 2435  df-clel 2438  df-nfc 2567  df-rex 2717
  Copyright terms: Public domain W3C validator