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

Theorem 2exbii 1844
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 1843 . 2 (∃𝑦𝜑 ↔ ∃𝑦𝜓)
32exbii 1843 1 (∃𝑥𝑦𝜑 ↔ ∃𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wex 1774
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804
This theorem depends on definitions:  df-bi 206  df-ex 1775
This theorem is referenced by:  3exbii  1845  2exanali  1856  4exdistrv  1953  3exdistr  1957  cbvex4vw  2038  eeeanv  2341  ee4anv  2342  2exsb  2351  cbvex4v  2409  2sb5rf  2466  sbel2x  2468  2mo2  2636  reeanlem  3216  rexcomf  3291  cgsex4g  3511  ceqsex3v  3523  ceqsex4v  3524  ceqsex8v  3526  copsexgw  5496  copsexg  5497  copsex2g  5499  vopelopabsb  5535  opabn0  5559  elxp2  5706  rabxp  5730  elxp3  5748  elvv  5756  elvvv  5757  copsex2gb  5812  elcnv2  5884  cnvuni  5893  cnvopab  6149  xpdifid  6179  coass  6276  fununi  6634  dfmpt3  6695  tpres  7218  dfoprab2  7483  dmoprab  7527  rnoprab  7529  mpomptx  7538  resoprab  7543  elrnmpores  7564  ov3  7589  ov6g  7590  uniuni  7770  opabex3rd  7980  oprabex3  7991  wfrlem4OLD  8342  oeeu  8633  xpassen  9104  sbthfilem  9235  zorn2lem6  10544  ltresr  11183  axaddf  11188  axmulf  11189  hashfun  14454  hash2prb  14491  5oalem7  31593  mpomptxf  32595  eulerpartlemgvv  34210  bnj600  34764  bnj916  34778  bnj983  34796  bnj986  34800  bnj996  34801  bnj1021  34811  dfacycgr1  34972  satfv1  35191  elima4  35599  brtxp2  35705  brpprod3a  35710  brpprod3b  35711  elfuns  35739  brcart  35756  brimg  35761  brapply  35762  brsuccf  35765  brrestrict  35773  dfrdg4  35775  ellines  35976  bj-cbvex4vv  36510  itg2addnclem3  37374  brxrn2  38073  dfxrn2  38074  ecxrn  38085  inxpxrn  38093  rnxrn  38096  dalem20  39392  dvhopellsm  40816  diblsmopel  40870  ralopabb  43078  en2pr  43214  pm11.52  44061  pm11.6  44066  pm11.7  44070  opelopab4  44227  stoweidlem35  45656  fundcmpsurbijinj  46982  mpomptx2  47713
  Copyright terms: Public domain W3C validator