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

Theorem 2rexbii 2889
Description: Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.)
Hypothesis
Ref Expression
rexbii.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 rexbii.1 . . 3  |-  ( ph  <->  ps )
21rexbii 2888 . 2  |-  ( E. y  e.  B  ph  <->  E. y  e.  B  ps )
32rexbii 2888 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 188   E.wrex 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1663  df-rex 2742
This theorem is referenced by:  ralnex2  2892  ralnex3  2893  3reeanv  2958  addcompr  9443  mulcompr  9445  4fvwrd4  11906  ntrivcvgmul  13951  prodmo  13983  pythagtriplem2  14760  pythagtrip  14777  isnsgrp  16524  efgrelexlemb  17393  ordthaus  20393  regr1lem2  20748  fmucndlem  21299  dfcgra2  24864  axpasch  24964  axeuclid  24986  axcontlem4  24990  frgrawopreglem5  25769  xrofsup  28346  poseq  30484  altopelaltxp  30736  brsegle  30868  mzpcompact2lem  35587  sbc4rex  35626  7rexfrabdioph  35637  expdiophlem1  35870  fourierdlem42  38006  fourierdlem42OLD  38007  usgr2edg1  39278  ldepslinc  40289
  Copyright terms: Public domain W3C validator