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

Theorem 2exbii 1594
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 1593 . 2  |-  ( E. y ph  <->  E. y ps )
32exbii 1593 1  |-  ( E. x E. y ph  <->  E. x E. y ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 178   E.wex 1551
This theorem is referenced by:  3exbii  1595  3exdistr  1934  eeeanv  1939  ee4anv  1941  cbvex4v  1997  sbel2x  2204  2eu4  2366  2eu6  2368  rexcomf  2869  reean  2876  ceqsex3v  2996  ceqsex4v  2997  ceqsex8v  2999  vtocl3  3010  copsexg  4445  opelopabsbOLD  4466  opabn0  4488  uniuni  4719  rabxp  4917  elxp3  4931  elvv  4939  elvvv  4940  elcnv2  5053  cnvuni  5060  coass  5391  fununi  5520  dfmpt3  5570  dfoprab2  6124  dmoprab  6157  rnoprab  6159  mpt2mptx  6167  resoprab  6169  oprabex3  6191  ov3  6213  ov6g  6214  copsex2gb  6410  oeeu  6849  xpassen  7205  zorn2lem6  8386  ltresr  9020  axaddf  9025  axmulf  9026  hashfun  11705  5oalem7  23167  elima4  25409  wfrlem4  25546  brtxp2  25731  brpprod3a  25736  brpprod3b  25737  elfuns  25765  brcart  25782  brimg  25787  brapply  25788  brsuccf  25791  brrestrict  25799  dfrdg4  25800  ellines  26091  itg2addnclem3  26272  pm11.52  27576  2exanali  27577  pm11.6  27582  pm11.7  27586  stoweidlem35  27774  opelopab4  28712  bnj600  29364  bnj916  29378  bnj983  29396  bnj986  29399  bnj996  29400  bnj1021  29409  sbel2xNEW7  29688  ee4anvOLD7  29779  cbvex4vOLD7  29812  dalem20  30564  dvhopellsm  31989  diblsmopel  32043
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567
This theorem depends on definitions:  df-bi 179  df-ex 1552
  Copyright terms: Public domain W3C validator