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  1962  3exdistr  1964  cbvex4v  1983  ee4anv  1987  ee8anv  1988  sbel2x  2051  2eu4  2173  rexcomf  2695  reean  2702  ceqsex3v  2846  ceqsex4v  2847  ceqsex8v  2849  copsexg  4336  opelopabsbALT  4353  opabm  4375  uniuni  4548  rabxp  4763  elxp3  4780  elvv  4788  elvvv  4789  rexiunxp  4872  elcnv2  4908  cnvuni  4916  coass  5255  fununi  5398  dfmpt3  5455  dfoprab2  6068  dmoprab  6102  rnoprab  6104  mpomptx  6112  resoprab  6117  ovi3  6159  ov6g  6160  oprabex3  6291  xpassen  7014  enq0enq  7651  enq0sym  7652  enq0tr  7654  ltresr  8059  axaddf  8088  axmulf  8089