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 205  ∃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 206  df-ex 1779

This theorem is referenced by:  3exbii  1849  2exanali  1860  4exdistrv  1957  3exdistr  1961  cbvex4vw  2042  eeeanv  2345  ee4anv  2346  2exsb  2355  cbvex4v  2412  2sb5rf  2469  sbel2x  2471  2mo2  2646  reeanlem  3211  rexcomf  3281  ceqsex3v  3488  ceqsex4v  3489  ceqsex8v  3491  copsexgw  5416  copsexg  5417  copsex2g  5419  vopelopabsb  5455  opabn0  5479  elxp2  5624  rabxp  5646  elxp3  5664  elvv  5672  elvvv  5673  copsex2gb  5728  elcnv2  5799  cnvuni  5808  xpdifid  6086  coass  6183  fununi  6538  dfmpt3  6597  tpres  7108  dfoprab2  7366  dmoprab  7409  rnoprab  7411  mpomptx  7420  resoprab  7425  elrnmpores  7444  ov3  7468  ov6g  7469  uniuni  7645  opabex3rd  7845  oprabex3  7856  wfrlem4OLD  8178  oeeu  8470  xpassen  8896  sbthfilem  9031  zorn2lem6  10317  ltresr  10956  axaddf  10961  axmulf  10962  hashfun  14211  hash2prb  14245  5oalem7  30120  mpomptxf  31114  eulerpartlemgvv  32439  bnj600  32995  bnj916  33009  bnj983  33027  bnj986  33031  bnj996  33032  bnj1021  33042  dfacycgr1  33202  satfv1  33421  elima4  33844  brtxp2  34242  brpprod3a  34247  brpprod3b  34248  elfuns  34276  brcart  34293  brimg  34298  brapply  34299  brsuccf  34302  brrestrict  34310  dfrdg4  34312  ellines  34513  bj-cbvex4vv  35046  itg2addnclem3  35888  brxrn2  36599  dfxrn2  36600  ecxrn  36611  inxpxrn  36619  rnxrn  36622  dalem20  37917  dvhopellsm  39341  diblsmopel  39395  en2pr  41380  pm11.52  42231  pm11.6  42236  pm11.7  42240  opelopab4  42397  stoweidlem35  43818  fundcmpsurbijinj  45119  mpomptx2  45927