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

Theorem 2exbii 1593
Description: Inference adding two existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.)
Hypothesis
Ref Expression
2exbii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
2exbii  |-  ( E. x E. y ph  <->  E. x E. y ps )

Proof of Theorem 2exbii
StepHypRef Expression
1 2exbii.1 . . 3  |-  ( ph  <->  ps )
21exbii 1592 . 2  |-  ( E. y ph  <->  E. y ps )
32exbii 1592 1  |-  ( E. x E. y ph  <->  E. x E. y ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   E.wex 1550
This theorem is referenced by:  3exbii  1594  3exdistr  1933  eeeanv  1938  ee4anv  1940  cbvex4v  1996  sbel2x  2201  2eu4  2363  2eu6  2365  rexcomf  2859  reean  2866  ceqsex3v  2986  ceqsex4v  2987  ceqsex8v  2989  vtocl3  3000  copsexg  4434  opelopabsbOLD  4455  opabn0  4477  uniuni  4708  rabxp  4906  elxp3  4920  elvv  4928  elvvv  4929  elcnv2  5042  cnvuni  5049  coass  5380  fununi  5509  dfmpt3  5559  dfoprab2  6113  dmoprab  6146  rnoprab  6148  mpt2mptx  6156  resoprab  6158  oprabex3  6180  ov3  6202  ov6g  6203  copsex2gb  6399  oeeu  6838  xpassen  7194  zorn2lem6  8373  ltresr  9007  axaddf  9012  axmulf  9013  hashfun  11692  5oalem7  23154  elima4  25396  wfrlem4  25533  brtxp2  25718  brpprod3a  25723  brpprod3b  25724  elfuns  25752  brcart  25769  brimg  25774  brapply  25775  brsuccf  25778  brrestrict  25786  dfrdg4  25787  ellines  26078  itg2addnclem3  26248  pm11.52  27553  2exanali  27554  pm11.6  27559  pm11.7  27563  stoweidlem35  27751  opelopab4  28575  bnj600  29227  bnj916  29241  bnj983  29259  bnj986  29262  bnj996  29263  bnj1021  29272  sbel2xNEW7  29551  ee4anvOLD7  29642  cbvex4vOLD7  29675  dalem20  30427  dvhopellsm  31852  diblsmopel  31906
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator