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

Theorem 2rexbii 2583
Description: Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.)
Hypothesis
Ref Expression
ralbii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
2rexbii  |-  ( E. x  e.  A  E. y  e.  B  ph  <->  E. x  e.  A  E. y  e.  B  ps )

Proof of Theorem 2rexbii
StepHypRef Expression
1 ralbii.1 . . 3  |-  ( ph  <->  ps )
21rexbii 2581 . 2  |-  ( E. y  e.  B  ph  <->  E. y  e.  B  ps )
32rexbii 2581 1  |-  ( E. x  e.  A  E. y  e.  B  ph  <->  E. x  e.  A  E. y  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   E.wrex 2557
This theorem is referenced by:  3reeanv  2721  addcompr  8661  mulcompr  8663  pythagtriplem2  12886  pythagtrip  12903  efgrelexlemb  15075  ordthaus  17128  regr1lem2  17447  prodmo  24159  poseq  24324  altopelaltxp  24582  axpasch  24641  axeuclid  24663  axcontlem4  24667  brsegle  24803  mzpcompact2lem  26932  7rexfrabdioph  26984  expdiophlem1  27217  4fvwrd4  28220
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-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-rex 2562
  Copyright terms: Public domain W3C validator