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  3489  ceqsex3v  3497  ceqsex4v  3498  ceqsex8v  3500  copsexgw  5446  copsexg  5447  copsex2g  5449  vopelopabsb  5485  opabn0  5509  elxp2  5656  rabxp  5680  elxp3  5698  elvv  5707  elvvv  5708  copsex2gb  5763  elcnv2  5834  cnvuni  5843  cnvopab  6102  xpdifid  6134  coass  6232  fununi  6575  dfmpt3  6634  tpres  7157  dfoprab2  7426  cbvoprab3v  7460  dmoprab  7471  rnoprab  7473  mpomptx  7481  resoprab  7486  elrnmpores  7506  ov3  7531  ov6g  7532  uniuni  7717  opabex3rd  7920  oprabex3  7931  oeeu  8541  xpassen  9011  sbthfilem  9134  zorn2lem6  10423  ltresr  11063  axaddf  11068  axmulf  11069  hashfun  14372  hash2prb  14407  5oalem7  31747  mpomptxf  32767  eulerpartlemgvv  34553  bnj600  35094  bnj916  35108  bnj983  35126  bnj986  35130  bnj996  35131  bnj1021  35141  dfacycgr1  35357  satfv1  35576  elima4  35989  brtxp2  36092  brpprod3a  36097  brpprod3b  36098  elfuns  36126  brcart  36143  brimg  36148  brapply  36149  lemsuccf  36152  brrestrict  36162  dfrdg4  36164  ellines  36365  bj-cbvex4vv  37047  copsex2gd  37387  itg2addnclem3  37918  brxrn2  38629  dfxrn2  38630  ecxrn  38651  inxpxrn  38663  rnxrn  38666  dmqsblocks  39212  dalem20  40063  dvhopellsm  41487  diblsmopel  41541  ralopabb  43761  en2pr  43897  pm11.52  44737  pm11.6  44742  pm11.7  44746  opelopab4  44901  stoweidlem35  46387  fundcmpsurbijinj  47764  mpomptx2  48689