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

Theorem 2exbii 1570
Description: Inference adding 2 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 1569 . 2  |-  ( E. y ph  <->  E. y ps )
32exbii 1569 1  |-  ( E. x E. y ph  <->  E. x E. y ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   E.wex 1528
This theorem is referenced by:  3exbii  1571  3exdistr  1851  ee4anv  1856  cbvex4v  1952  sbel2x  2064  2eu4  2226  2eu6  2228  rexcomf  2699  reean  2706  ceqsex3v  2826  ceqsex4v  2827  ceqsex8v  2829  vtocl3  2840  copsexg  4252  opelopabsbOLD  4273  opabn0  4295  uniuni  4527  rabxp  4725  elxp3  4739  elvv  4748  elvvv  4749  elcnv2  4859  cnvuni  4866  coass  5191  fununi  5316  dfmpt3  5366  dfoprab2  5895  dmoprab  5928  rnoprab  5930  mpt2mptx  5938  resoprab  5940  oprabex3  5962  ov3  5984  ov6g  5985  copsex2gb  6180  oeeu  6601  xpassen  6956  zorn2lem6  8128  ltresr  8762  axaddf  8767  axmulf  8768  hashfun  11389  5oalem7  22239  wfrlem4  24259  brtxp2  24421  brpprod3a  24426  brpprod3b  24427  elfuns  24454  brcart  24471  brimg  24476  brapply  24477  brsuccf  24480  brrestrict  24487  dfrdg4  24488  ellines  24775  dfoprab4pop  25037  pm11.52  27585  2exanali  27586  pm11.6  27591  pm11.7  27595  stoweidlem35  27784  opelopab4  28317  bnj600  28951  bnj916  28965  bnj983  28983  bnj986  28986  bnj996  28987  bnj1021  28996  dalem20  29882  dvhopellsm  31307  diblsmopel  31361
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-ex 1529
  Copyright terms: Public domain W3C validator