Theorem 2exbii 1847

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

Step	Hyp	Ref	Expression
1		2exbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	exbii 1846	. 2 ⊢ (∃𝑦𝜑 ↔ ∃𝑦𝜓)
3	2	exbii 1846	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓)

Syntax hints:   ↔ wb 206  ∃wex 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807

This theorem depends on definitions:  df-bi 207  df-ex 1778

This theorem is referenced by:  3exbii  1848  2exanali  1859  4exdistrv  1956  3exdistr  1960  cbvex4vw  2041  eeeanv  2356  ee4anv  2357  2exsb  2366  cbvex4v  2423  2sb5rf  2480  sbel2x  2482  2mo2  2650  r3ex  3204  reeanlem  3234  rexcomf  3309  cgsex4g  3538  ceqsex3v  3549  ceqsex4v  3550  ceqsex8v  3552  copsexgw  5510  copsexg  5511  copsex2g  5513  vopelopabsb  5548  opabn0  5572  elxp2  5724  rabxp  5748  elxp3  5766  elvv  5774  elvvv  5775  copsex2gb  5830  elcnv2  5902  cnvuni  5911  cnvopab  6169  xpdifid  6199  coass  6296  fununi  6653  dfmpt3  6714  tpres  7238  dfoprab2  7508  cbvoprab3v  7542  dmoprab  7552  rnoprab  7554  mpomptx  7563  resoprab  7568  elrnmpores  7588  ov3  7613  ov6g  7614  uniuni  7797  opabex3rd  8007  oprabex3  8018  wfrlem4OLD  8368  oeeu  8659  xpassen  9132  sbthfilem  9264  zorn2lem6  10570  ltresr  11209  axaddf  11214  axmulf  11215  hashfun  14486  hash2prb  14521  5oalem7  31692  mpomptxf  32695  eulerpartlemgvv  34341  bnj600  34895  bnj916  34909  bnj983  34927  bnj986  34931  bnj996  34932  bnj1021  34942  dfacycgr1  35112  satfv1  35331  elima4  35739  brtxp2  35845  brpprod3a  35850  brpprod3b  35851  elfuns  35879  brcart  35896  brimg  35901  brapply  35902  brsuccf  35905  brrestrict  35913  dfrdg4  35915  ellines  36116  bj-cbvex4vv  36771  itg2addnclem3  37633  brxrn2  38331  dfxrn2  38332  ecxrn  38343  inxpxrn  38351  rnxrn  38354  dalem20  39650  dvhopellsm  41074  diblsmopel  41128  ralopabb  43373  en2pr  43509  pm11.52  44356  pm11.6  44361  pm11.7  44365  opelopab4  44522  stoweidlem35  45956  fundcmpsurbijinj  47284  mpomptx2  48059