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  30944  mpomptxf  31936  eulerpartlemgvv  33406  bnj600  33961  bnj916  33975  bnj983  33993  bnj986  33997  bnj996  33998  bnj1021  34008  dfacycgr1  34166  satfv1  34385  elima4  34778  brtxp2  34884  brpprod3a  34889  brpprod3b  34890  elfuns  34918  brcart  34935  brimg  34940  brapply  34941  brsuccf  34944  brrestrict  34952  dfrdg4  34954  ellines  35155  bj-cbvex4vv  35731  itg2addnclem3  36589  brxrn2  37293  dfxrn2  37294  ecxrn  37305  inxpxrn  37313  rnxrn  37316  dalem20  38612  dvhopellsm  40036  diblsmopel  40090  ralopabb  42210  en2pr  42346  pm11.52  43194  pm11.6  43199  pm11.7  43203  opelopab4  43360  stoweidlem35  44799  fundcmpsurbijinj  46126  mpomptx2  47058