Theorem 2exbii 1599

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

Syntax hints:   ↔ wb 104  ∃wex 1485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-ial 1527

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3exbii  1600  19.42vvvv  1906  3exdistr  1908  cbvex4v  1923  ee4anv  1927  ee8anv  1928  sbel2x  1991  2eu4  2112  rexcomf  2632  reean  2638  ceqsex3v  2772  ceqsex4v  2773  ceqsex8v  2775  copsexg  4229  opelopabsbALT  4244  opabm  4265  uniuni  4436  rabxp  4648  elxp3  4665  elvv  4673  elvvv  4674  rexiunxp  4753  elcnv2  4789  cnvuni  4797  coass  5129  fununi  5266  dfmpt3  5320  dfoprab2  5900  dmoprab  5934  rnoprab  5936  mpomptx  5944  resoprab  5949  ovi3  5989  ov6g  5990  oprabex3  6108  xpassen  6808  enq0enq  7393  enq0sym  7394  enq0tr  7396  ltresr  7801  axaddf  7830  axmulf  7831