Theorem 2exbii 1655

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

Syntax hints:   ↔ wb 105  ∃wex 1541

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3exbii  1656  19.42vvvv  1963  3exdistr  1965  cbvex4v  1984  ee4anv  1988  ee8anv  1989  sbel2x  2052  2eu4  2174  rexcomf  2705  reean  2712  ceqsex3v  2856  ceqsex4v  2857  ceqsex8v  2859  copsexg  4359  opelopabsbALT  4376  opabm  4398  uniuni  4571  rabxp  4786  elxp3  4803  elvv  4811  elvvv  4812  rexiunxp  4896  elcnv2  4932  cnvuni  4940  coass  5280  fununi  5423  dfmpt3  5480  dfoprab2  6099  dmoprab  6133  rnoprab  6135  mpomptx  6143  resoprab  6148  ovi3  6190  ov6g  6191  oprabex3  6321  xpassen  7080  enq0enq  7742  enq0sym  7743  enq0tr  7745  ltresr  8150  axaddf  8179  axmulf  8180