Theorem 2exbii 1852

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

Syntax hints:   ↔ wb 205  ∃wex 1782

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

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  3exbii  1853  2exanali  1864  4exdistrv  1961  3exdistr  1965  cbvex4vw  2046  eeeanv  2347  ee4anv  2348  2exsb  2357  cbvex4v  2415  2sb5rf  2472  sbel2x  2474  2mo2  2644  reeanlem  3226  rexcomf  3301  cgsex4g  3521  ceqsex3v  3532  ceqsex4v  3533  ceqsex8v  3535  copsexgw  5491  copsexg  5492  copsex2g  5494  vopelopabsb  5530  opabn0  5554  elxp2  5701  rabxp  5725  elxp3  5743  elvv  5751  elvvv  5752  copsex2gb  5807  elcnv2  5878  cnvuni  5887  xpdifid  6168  coass  6265  fununi  6624  dfmpt3  6685  tpres  7202  dfoprab2  7467  dmoprab  7510  rnoprab  7512  mpomptx  7521  resoprab  7526  elrnmpores  7546  ov3  7570  ov6g  7571  uniuni  7749  opabex3rd  7953  oprabex3  7964  wfrlem4OLD  8312  oeeu  8603  xpassen  9066  sbthfilem  9201  zorn2lem6  10496  ltresr  11135  axaddf  11140  axmulf  11141  hashfun  14397  hash2prb  14433  5oalem7  30913  mpomptxf  31905  eulerpartlemgvv  33375  bnj600  33930  bnj916  33944  bnj983  33962  bnj986  33966  bnj996  33967  bnj1021  33977  dfacycgr1  34135  satfv1  34354  elima4  34747  brtxp2  34853  brpprod3a  34858  brpprod3b  34859  elfuns  34887  brcart  34904  brimg  34909  brapply  34910  brsuccf  34913  brrestrict  34921  dfrdg4  34923  ellines  35124  bj-cbvex4vv  35683  itg2addnclem3  36541  brxrn2  37245  dfxrn2  37246  ecxrn  37257  inxpxrn  37265  rnxrn  37268  dalem20  38564  dvhopellsm  39988  diblsmopel  40042  ralopabb  42162  en2pr  42298  pm11.52  43146  pm11.6  43151  pm11.7  43155  opelopab4  43312  stoweidlem35  44751  fundcmpsurbijinj  46078  mpomptx2  47010