Theorem 2exbii 1851

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

Syntax hints:   ↔ wb 206  ∃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 207  df-ex 1782

This theorem is referenced by:  3exbii  1852  2exanali  1862  4exdistrv  1958  3exdistr  1962  cbvex4vw  2044  eeeanv  2355  ee4anv  2356  ee4anvOLD  2357  2exsb  2365  cbvex4v  2420  2sb5rf  2477  sbel2x  2479  2mo2  2648  r3ex  3177  reeanlem  3209  rexcomf  3277  cgsex4g  3477  ceqsex3v  3484  ceqsex4v  3485  ceqsex8v  3487  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  7149  dfoprab2  7418  cbvoprab3v  7452  dmoprab  7463  rnoprab  7465  mpomptx  7473  resoprab  7478  elrnmpores  7498  ov3  7523  ov6g  7524  uniuni  7709  opabex3rd  7912  oprabex3  7923  oeeu  8532  xpassen  9002  sbthfilem  9125  zorn2lem6  10414  ltresr  11054  axaddf  11059  axmulf  11060  hashfun  14390  hash2prb  14425  5oalem7  31746  mpomptxf  32766  eulerpartlemgvv  34536  bnj600  35077  bnj916  35091  bnj983  35109  bnj986  35113  bnj996  35114  bnj1021  35124  dfacycgr1  35342  satfv1  35561  elima4  35974  brtxp2  36077  brpprod3a  36082  brpprod3b  36083  elfuns  36111  brcart  36128  brimg  36133  brapply  36134  lemsuccf  36137  brrestrict  36147  dfrdg4  36149  ellines  36350  bj-cbvex4vv  37128  copsex2gd  37468  itg2addnclem3  38008  brxrn2  38719  dfxrn2  38720  ecxrn  38741  inxpxrn  38753  rnxrn  38756  dmqsblocks  39302  dalem20  40153  dvhopellsm  41577  diblsmopel  41631  ralopabb  43856  en2pr  43992  pm11.52  44832  pm11.6  44837  pm11.7  44841  opelopab4  44996  stoweidlem35  46481  fundcmpsurbijinj  47882  mpomptx2  48823