Theorem 2exbii 1654

Description: Inference adding 2 existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.)

Hypothesis

Ref	Expression
exbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
2exbii	⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓)

Proof of Theorem 2exbii

Step	Hyp	Ref	Expression
1		exbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	exbii 1653	. 2 ⊢ (∃𝑦𝜑 ↔ ∃𝑦𝜓)
3	2	exbii 1653	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓)

Syntax hints:   ↔ wb 105  ∃wex 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-ial 1582

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3exbii  1655  19.42vvvv  1961  3exdistr  1963  cbvex4v  1982  ee4anv  1986  ee8anv  1987  sbel2x  2050  2eu4  2172  rexcomf  2694  reean  2701  ceqsex3v  2845  ceqsex4v  2846  ceqsex8v  2848  copsexg  4338  opelopabsbALT  4355  opabm  4377  uniuni  4550  rabxp  4765  elxp3  4782  elvv  4790  elvvv  4791  rexiunxp  4874  elcnv2  4910  cnvuni  4918  coass  5257  fununi  5400  dfmpt3  5457  dfoprab2  6073  dmoprab  6107  rnoprab  6109  mpomptx  6117  resoprab  6122  ovi3  6164  ov6g  6165  oprabex3  6296  xpassen  7019  enq0enq  7656  enq0sym  7657  enq0tr  7659  ltresr  8064  axaddf  8093  axmulf  8094