Theorem 2exbii 1879

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 1878	. 2 ⊢ (∃𝑦𝜑 ↔ ∃𝑦𝜓)
3	2	exbii 1878	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓)

Syntax hints:   ↔ wb 209  ∃wex 1809

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

This theorem depends on definitions:  df-bi 210  df-ex 1810

This theorem is referenced by:  3exbii  1880  2exanali  1890  4exdistrv  1986  3exdistr  1990  cbvex4vw  2072  eeeanv  2382  ee4anv  2383  ee4anvOLD  2384  2exsb  2392  cbvex4v  2447  2sb5rf  2504  sbel2x  2506  2mo2  2675  r3ex  3204  reeanlem  3236  rexcomf  3304  cgsex4g  3501  ceqsex3v  3507  ceqsex4v  3508  ceqsex8v  3510  copsexgw  5474  copsexgwOLD  5475  copsexg  5476  copsex2g  5478  vopelopabsb  5515  opabn0  5540  elxp2  5687  rabxp  5711  elxp3  5729  elvv  5738  elvvv  5739  copsex2gb  5795  elcnv2  5865  cnvuni  5878  cnvopab  6139  xpdifid  6167  xpdifcnvepel  6168  coass  6269  fununi  6613  dfmpt3  6671  tpres  7201  dfoprab2  7470  cbvoprab3v  7504  dmoprab  7515  rnoprab  7517  mpomptx  7525  resoprab  7530  elrnmpores  7550  ov3  7575  ov6g  7576  uniuni  7762  opabex3rd  7964  oprabex3  7975  oeeu  8590  xpassen  9060  sbthfilem  9183  zorn2lem6  10486  ltresr  11126  axaddf  11131  axmulf  11132  hashfun  14476  hash2prb  14511  5oalem7  31990  mpomptxf  33001  eulerpartlemgvv  34744  bnj600  35285  bnj916  35299  bnj983  35317  bnj986  35321  bnj996  35322  bnj1021  35332  dfacycgr1  35614  satfv1  35833  elima4  36246  brtxp2  36349  brpprod3a  36354  brpprod3b  36355  elfuns  36383  brcart  36400  brimg  36405  brapply  36406  lemsuccf  36409  brrestrict  36419  dfrdg4  36421  ellines  36622  bj-cbvex4vv  37418  copsex2gd  37760  itg2addnclem3  38302  brxrn2  39011  dfxrn2  39012  ecxrn  39033  inxpxrn  39045  rnxrn  39048  dmqsblocks  39594  dalem20  40445  dvhopellsm  41869  diblsmopel  41923  ralopabb  44117  en2pr  44253  pm11.52  45077  pm11.6  45082  pm11.7  45086  opelopab4  45240  stoweidlem35  46729  fundcmpsurbijinj  48136  mpomptx2  49092