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

Theorem 2rexbii 2677
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 2675 . 2  |-  ( E. y  e.  B  ph  <->  E. y  e.  B  ps )
32rexbii 2675 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 177   E.wrex 2651
This theorem is referenced by:  3reeanv  2820  addcompr  8832  mulcompr  8834  4fvwrd4  11052  pythagtriplem2  13119  pythagtrip  13136  efgrelexlemb  15310  ordthaus  17371  regr1lem2  17694  fmucndlem  18243  xrofsup  23963  ntrivcvgmul  25010  prodmo  25042  poseq  25278  altopelaltxp  25536  axpasch  25595  axeuclid  25617  axcontlem4  25621  brsegle  25757  mzpcompact2lem  26500  7rexfrabdioph  26552  expdiophlem1  26784  frgrawopreglem5  27801
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-rex 2656
  Copyright terms: Public domain W3C validator