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  2352  ee4anv  2353  ee4anvOLD  2354  2exsb  2362  cbvex4v  2417  2sb5rf  2474  sbel2x  2476  2mo2  2644  r3ex  3172  reeanlem  3204  rexcomf  3272  cgsex4g  3484  ceqsex3v  3492  ceqsex4v  3493  ceqsex8v  3495  copsexgw  5433  copsexg  5434  copsex2g  5436  vopelopabsb  5472  opabn0  5496  elxp2  5643  rabxp  5667  elxp3  5685  elvv  5694  elvvv  5695  copsex2gb  5750  elcnv2  5821  cnvuni  5830  cnvopab  6088  xpdifid  6120  coass  6218  fununi  6561  dfmpt3  6620  tpres  7141  dfoprab2  7410  cbvoprab3v  7444  dmoprab  7455  rnoprab  7457  mpomptx  7465  resoprab  7470  elrnmpores  7490  ov3  7515  ov6g  7516  uniuni  7701  opabex3rd  7904  oprabex3  7915  oeeu  8524  xpassen  8991  sbthfilem  9114  zorn2lem6  10399  ltresr  11038  axaddf  11043  axmulf  11044  hashfun  14346  hash2prb  14381  5oalem7  31642  mpomptxf  32663  eulerpartlemgvv  34410  bnj600  34952  bnj916  34966  bnj983  34984  bnj986  34988  bnj996  34989  bnj1021  34999  dfacycgr1  35209  satfv1  35428  elima4  35841  brtxp2  35944  brpprod3a  35949  brpprod3b  35950  elfuns  35978  brcart  35995  brimg  36000  brapply  36001  lemsuccf  36004  brrestrict  36014  dfrdg4  36016  ellines  36217  bj-cbvex4vv  36870  itg2addnclem3  37733  brxrn2  38428  dfxrn2  38429  ecxrn  38450  inxpxrn  38462  rnxrn  38465  dmqsblocks  38971  dalem20  39812  dvhopellsm  41236  diblsmopel  41290  ralopabb  43528  en2pr  43664  pm11.52  44504  pm11.6  44509  pm11.7  44513  opelopab4  44668  stoweidlem35  46157  fundcmpsurbijinj  47534  mpomptx2  48459