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

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

Syntax hints:   ↔ wb 206  ∃wex 1780

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

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

This theorem is referenced by:  3exbii  1851  2exanali  1861  4exdistrv  1957  3exdistr  1961  cbvex4vw  2043  eeeanv  2354  ee4anv  2355  ee4anvOLD  2356  2exsb  2364  cbvex4v  2419  2sb5rf  2476  sbel2x  2478  2mo2  2647  r3ex  3175  reeanlem  3207  rexcomf  3275  cgsex4g  3487  ceqsex3v  3495  ceqsex4v  3496  ceqsex8v  3498  copsexgw  5438  copsexg  5439  copsex2g  5441  vopelopabsb  5477  opabn0  5501  elxp2  5648  rabxp  5672  elxp3  5690  elvv  5699  elvvv  5700  copsex2gb  5755  elcnv2  5826  cnvuni  5835  cnvopab  6094  xpdifid  6126  coass  6224  fununi  6567  dfmpt3  6626  tpres  7147  dfoprab2  7416  cbvoprab3v  7450  dmoprab  7461  rnoprab  7463  mpomptx  7471  resoprab  7476  elrnmpores  7496  ov3  7521  ov6g  7522  uniuni  7707  opabex3rd  7910  oprabex3  7921  oeeu  8531  xpassen  8999  sbthfilem  9122  zorn2lem6  10411  ltresr  11051  axaddf  11056  axmulf  11057  hashfun  14360  hash2prb  14395  5oalem7  31735  mpomptxf  32757  eulerpartlemgvv  34533  bnj600  35075  bnj916  35089  bnj983  35107  bnj986  35111  bnj996  35112  bnj1021  35122  dfacycgr1  35338  satfv1  35557  elima4  35970  brtxp2  36073  brpprod3a  36078  brpprod3b  36079  elfuns  36107  brcart  36124  brimg  36129  brapply  36130  lemsuccf  36133  brrestrict  36143  dfrdg4  36145  ellines  36346  bj-cbvex4vv  37006  itg2addnclem3  37870  brxrn2  38565  dfxrn2  38566  ecxrn  38587  inxpxrn  38599  rnxrn  38602  dmqsblocks  39108  dalem20  39949  dvhopellsm  41373  diblsmopel  41427  ralopabb  43648  en2pr  43784  pm11.52  44624  pm11.6  44629  pm11.7  44633  opelopab4  44788  stoweidlem35  46275  fundcmpsurbijinj  47652  mpomptx2  48577