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

Theorem 2exbii 1850
 Description: Inference adding two existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.)
Hypothesis
Ref Expression
2exbii.1 (𝜑𝜓)
Assertion
Ref Expression
2exbii (∃𝑥𝑦𝜑 ↔ ∃𝑥𝑦𝜓)

Proof of Theorem 2exbii
StepHypRef Expression
1 2exbii.1 . . 3 (𝜑𝜓)
21exbii 1849 . 2 (∃𝑦𝜑 ↔ ∃𝑦𝜓)
32exbii 1849 1 (∃𝑥𝑦𝜑 ↔ ∃𝑥𝑦𝜓)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209  ∃wex 1781 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811 This theorem depends on definitions:  df-bi 210  df-ex 1782 This theorem is referenced by:  3exbii  1851  2exanali  1861  4exdistrv  1957  3exdistr  1962  cbvex4vw  2049  eeeanv  2360  ee4anv  2361  2exsb  2368  cbvex4v  2426  2sb5rf  2485  sbel2x  2487  2mo2  2709  rexcomOLD  3309  rexcomf  3311  reeanlem  3318  ceqsex3v  3493  ceqsex4v  3494  ceqsex8v  3496  copsexgw  5347  copsexg  5348  opelopabsbALT  5382  opabn0  5406  elxp2  5544  rabxp  5565  elxp3  5583  elvv  5591  elvvv  5592  copsex2gb  5644  elcnv2  5713  cnvuni  5722  xpdifid  5993  coass  6088  fununi  6402  dfmpt3  6457  tpres  6945  dfoprab2  7196  dmoprab  7239  rnoprab  7241  mpomptx  7249  resoprab  7254  elrnmpores  7273  ov3  7297  ov6g  7298  uniuni  7471  opabex3rd  7656  oprabex3  7667  wfrlem4  7948  oeeu  8219  xpassen  8601  zorn2lem6  9919  ltresr  10558  axaddf  10563  axmulf  10564  hashfun  13801  hash2prb  13833  5oalem7  29457  mpomptxf  30456  eulerpartlemgvv  31780  bnj600  32337  bnj916  32351  bnj983  32369  bnj986  32373  bnj996  32374  bnj1021  32384  dfacycgr1  32540  satfv1  32759  elima4  33168  brtxp2  33491  brpprod3a  33496  brpprod3b  33497  elfuns  33525  brcart  33542  brimg  33547  brapply  33548  brsuccf  33551  brrestrict  33559  dfrdg4  33561  ellines  33762  bj-cbvex4vv  34282  itg2addnclem3  35150  brxrn2  35827  dfxrn2  35828  ecxrn  35839  inxpxrn  35843  rnxrn  35846  dalem20  37029  dvhopellsm  38453  diblsmopel  38507  en2pr  40310  pm11.52  41155  pm11.6  41160  pm11.7  41164  opelopab4  41321  stoweidlem35  42738  fundcmpsurbijinj  43988  mpomptx2  44797
 Copyright terms: Public domain W3C validator