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

Theorem 2exbii 1848
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 1847 . 2 (∃𝑦𝜑 ↔ ∃𝑦𝜓)
32exbii 1847 1 (∃𝑥𝑦𝜑 ↔ ∃𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wex 1778
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808
This theorem depends on definitions:  df-bi 207  df-ex 1779
This theorem is referenced by:  3exbii  1849  2exanali  1859  4exdistrv  1955  3exdistr  1959  cbvex4vw  2040  eeeanv  2351  ee4anv  2352  ee4anvOLD  2353  2exsb  2362  cbvex4v  2419  2sb5rf  2476  sbel2x  2478  2mo2  2646  r3ex  3197  reeanlem  3227  rexcomf  3302  cgsex4g  3527  ceqsex3v  3536  ceqsex4v  3537  ceqsex8v  3539  copsexgw  5494  copsexg  5495  copsex2g  5497  vopelopabsb  5533  opabn0  5557  elxp2  5708  rabxp  5732  elxp3  5750  elvv  5759  elvvv  5760  copsex2gb  5815  elcnv2  5887  cnvuni  5896  cnvopab  6156  xpdifid  6187  coass  6284  fununi  6640  dfmpt3  6701  tpres  7222  dfoprab2  7492  cbvoprab3v  7526  dmoprab  7537  rnoprab  7539  mpomptx  7547  resoprab  7552  elrnmpores  7572  ov3  7597  ov6g  7598  uniuni  7783  opabex3rd  7992  oprabex3  8003  wfrlem4OLD  8353  oeeu  8642  xpassen  9107  sbthfilem  9239  zorn2lem6  10542  ltresr  11181  axaddf  11186  axmulf  11187  hashfun  14477  hash2prb  14512  5oalem7  31680  mpomptxf  32688  eulerpartlemgvv  34379  bnj600  34934  bnj916  34948  bnj983  34966  bnj986  34970  bnj996  34971  bnj1021  34981  dfacycgr1  35150  satfv1  35369  elima4  35777  brtxp2  35883  brpprod3a  35888  brpprod3b  35889  elfuns  35917  brcart  35934  brimg  35939  brapply  35940  brsuccf  35943  brrestrict  35951  dfrdg4  35953  ellines  36154  bj-cbvex4vv  36807  itg2addnclem3  37681  brxrn2  38377  dfxrn2  38378  ecxrn  38389  inxpxrn  38397  rnxrn  38400  dalem20  39696  dvhopellsm  41120  diblsmopel  41174  ralopabb  43429  en2pr  43565  pm11.52  44411  pm11.6  44416  pm11.7  44420  opelopab4  44576  stoweidlem35  46055  fundcmpsurbijinj  47402  mpomptx2  48256
  Copyright terms: Public domain W3C validator