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

Theorem 2rexbii 2570
Description: Inference adding 2 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 2568 . 2  |-  ( E. y  e.  B  ph  <->  E. y  e.  B  ps )
32rexbii 2568 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 2544
This theorem is referenced by:  3reeanv  2708  addcompr  8645  mulcompr  8647  pythagtriplem2  12870  pythagtrip  12887  efgrelexlemb  15059  ordthaus  17112  regr1lem2  17431  poseq  24253  altopelaltxp  24510  axpasch  24569  axeuclid  24591  axcontlem4  24595  brsegle  24731  mzpcompact2lem  26829  7rexfrabdioph  26881  expdiophlem1  27114
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-rex 2549
  Copyright terms: Public domain W3C validator