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

Theorem rexeqbidv 2762
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 2756 . 2  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  B  ps )
)
3 raleqbidv.2 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
43rexbidv 2577 . 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 1632   E.wrex 2557
This theorem is referenced by:  fpwwe2lem13  8280  vdwpc  13043  ramval  13071  mreexexlemd  13562  iscat  13590  iscatd  13591  catidex  13592  ismnd  14385  mndpropd  14414  gsumval2a  14475  isgrp  14509  isgrpd2e  14520  cayleyth  14806  iscyg  15182  ltbval  16229  opsrval  16232  is1stc  17183  2ndc1stc  17193  2ndcsep  17201  islly  17210  isnlly  17211  imasdsf1olem  17953  met2ndc  18085  evthicc  18835  isplig  20860  isgrp2d  20918  isgrpda  20980  isexid  21000  isrngo  21061  isrngod  21062  nmoofval  21356  iscvm  23805  cvmlift2lem13  23861  br8  24184  br6  24185  br4  24186  brsegle  24803  hilbert1.1  24849  isdir2  25395  dffprod  25422  cnegvex2b  25765  rnegvex2b  25766  isiso  25928  isfuna  25937  bisig0  26165  cover2g  26462  mzpcompact2lem  26932  eldioph  26940  supeq123d  27261  aomclem8  27262  psgnfval  27526  nb3graprlem2  28288  frgra2v  28423  1vwmgra  28427  3vfriswmgra  28429  lshpset  29790  cvrfval  30080  isatl  30111  ishlat1  30164  llnset  30316  lplnset  30340  lvolset  30383  lineset  30549  lcfl7N  32313  lcfrlem8  32361  lcfrlem9  32362  lcf1o  32363  hvmapffval  32570  hvmapfval  32571  hvmapval  32572
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562
  Copyright terms: Public domain W3C validator