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 209  ∃wex 1781

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

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

This theorem is referenced by:  3exbii  1851  2exanali  1861  4exdistrv  1957  3exdistr  1962  cbvex4vw  2049  eeeanv  2360  ee4anv  2361  2exsb  2368  cbvex4v  2426  2sb5rf  2485  sbel2x  2487  2mo2  2709  rexcomOLD  3309  rexcomf  3311  reeanlem  3318  ceqsex3v  3493  ceqsex4v  3494  ceqsex8v  3496  copsexgw  5346  copsexg  5347  opelopabsbALT  5381  opabn0  5405  elxp2  5543  rabxp  5564  elxp3  5582  elvv  5590  elvvv  5591  copsex2gb  5643  elcnv2  5712  cnvuni  5721  xpdifid  5992  coass  6085  fununi  6399  dfmpt3  6454  tpres  6940  dfoprab2  7191  dmoprab  7234  rnoprab  7236  mpomptx  7244  resoprab  7249  elrnmpores  7267  ov3  7291  ov6g  7292  uniuni  7464  opabex3rd  7649  oprabex3  7660  wfrlem4  7941  oeeu  8212  xpassen  8594  zorn2lem6  9912  ltresr  10551  axaddf  10556  axmulf  10557  hashfun  13794  hash2prb  13826  5oalem7  29443  mpomptxf  30442  eulerpartlemgvv  31744  bnj600  32301  bnj916  32315  bnj983  32333  bnj986  32337  bnj996  32338  bnj1021  32348  dfacycgr1  32504  satfv1  32723  elima4  33132  brtxp2  33455  brpprod3a  33460  brpprod3b  33461  elfuns  33489  brcart  33506  brimg  33511  brapply  33512  brsuccf  33515  brrestrict  33523  dfrdg4  33525  ellines  33726  bj-cbvex4vv  34242  itg2addnclem3  35110  brxrn2  35787  dfxrn2  35788  ecxrn  35799  inxpxrn  35803  rnxrn  35806  dalem20  36989  dvhopellsm  38413  diblsmopel  38467  en2pr  40246  pm11.52  41091  pm11.6  41096  pm11.7  41100  opelopab4  41257  stoweidlem35  42677  fundcmpsurbijinj  43927  mpomptx2  44736