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

Theorem 2rexbii 2740
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 2738 . 2  |-  ( E. y  e.  B  ph  <->  E. y  e.  B  ps )
32rexbii 2738 1  |-  ( E. x  e.  A  E. y  e.  B  ph  <->  E. x  e.  A  E. y  e.  B  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   E.wrex 2714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-rex 2719
This theorem is referenced by:  3reeanv  2887  addcompr  9188  mulcompr  9190  4fvwrd4  11531  pythagtriplem2  13882  pythagtrip  13899  efgrelexlemb  16245  ordthaus  18986  regr1lem2  19311  fmucndlem  19864  axpasch  23185  axeuclid  23207  axcontlem4  23211  xrofsup  26053  ntrivcvgmul  27415  prodmo  27447  poseq  27712  altopelaltxp  28005  brsegle  28137  mzpcompact2lem  29085  sbc4rex  29124  7rexfrabdioph  29135  expdiophlem1  29367  frgrawopreglem5  30638  ldepslinc  31048
  Copyright terms: Public domain W3C validator