Theorem 2exbii 1848

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

Syntax hints:   ↔ wb 206  ∃wex 1778

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

This theorem depends on definitions:  df-bi 207  df-ex 1779

This theorem is referenced by:  3exbii  1849  2exanali  1859  4exdistrv  1955  3exdistr  1959  cbvex4vw  2040  eeeanv  2351  ee4anv  2352  ee4anvOLD  2353  2exsb  2362  cbvex4v  2419  2sb5rf  2476  sbel2x  2478  2mo2  2646  r3ex  3197  reeanlem  3227  rexcomf  3302  cgsex4g  3527  ceqsex3v  3536  ceqsex4v  3537  ceqsex8v  3539  copsexgw  5494  copsexg  5495  copsex2g  5497  vopelopabsb  5533  opabn0  5557  elxp2  5708  rabxp  5732  elxp3  5750  elvv  5759  elvvv  5760  copsex2gb  5815  elcnv2  5887  cnvuni  5896  cnvopab  6156  xpdifid  6187  coass  6284  fununi  6640  dfmpt3  6701  tpres  7222  dfoprab2  7492  cbvoprab3v  7526  dmoprab  7537  rnoprab  7539  mpomptx  7547  resoprab  7552  elrnmpores  7572  ov3  7597  ov6g  7598  uniuni  7783  opabex3rd  7992  oprabex3  8003  wfrlem4OLD  8353  oeeu  8642  xpassen  9107  sbthfilem  9239  zorn2lem6  10542  ltresr  11181  axaddf  11186  axmulf  11187  hashfun  14477  hash2prb  14512  5oalem7  31680  mpomptxf  32688  eulerpartlemgvv  34379  bnj600  34934  bnj916  34948  bnj983  34966  bnj986  34970  bnj996  34971  bnj1021  34981  dfacycgr1  35150  satfv1  35369  elima4  35777  brtxp2  35883  brpprod3a  35888  brpprod3b  35889  elfuns  35917  brcart  35934  brimg  35939  brapply  35940  brsuccf  35943  brrestrict  35951  dfrdg4  35953  ellines  36154  bj-cbvex4vv  36807  itg2addnclem3  37681  brxrn2  38377  dfxrn2  38378  ecxrn  38389  inxpxrn  38397  rnxrn  38400  dalem20  39696  dvhopellsm  41120  diblsmopel  41174  ralopabb  43429  en2pr  43565  pm11.52  44411  pm11.6  44416  pm11.7  44420  opelopab4  44576  stoweidlem35  46055  fundcmpsurbijinj  47402  mpomptx2  48256