Theorem 2exbii 1606

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

Syntax hints:   ↔ wb 105  ∃wex 1492

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-ial 1534

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3exbii  1607  19.42vvvv  1913  3exdistr  1915  cbvex4v  1930  ee4anv  1934  ee8anv  1935  sbel2x  1998  2eu4  2119  rexcomf  2639  reean  2646  ceqsex3v  2781  ceqsex4v  2782  ceqsex8v  2784  copsexg  4246  opelopabsbALT  4261  opabm  4282  uniuni  4453  rabxp  4665  elxp3  4682  elvv  4690  elvvv  4691  rexiunxp  4771  elcnv2  4807  cnvuni  4815  coass  5149  fununi  5286  dfmpt3  5340  dfoprab2  5924  dmoprab  5958  rnoprab  5960  mpomptx  5968  resoprab  5973  ovi3  6013  ov6g  6014  oprabex3  6132  xpassen  6832  enq0enq  7432  enq0sym  7433  enq0tr  7435  ltresr  7840  axaddf  7869  axmulf  7870