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  1965  3exdistr  1967  cbvex4v  1986  ee4anv  1990  ee8anv  1991  sbel2x  2054  2eu4  2176  rexcomf  2707  reean  2714  ceqsex3v  2859  ceqsex4v  2860  ceqsex8v  2862  copsexg  4362  opelopabsbALT  4379  opabm  4401  uniuni  4574  rabxp  4789  elxp3  4806  elvv  4814  elvvv  4815  rexiunxp  4899  elcnv2  4935  cnvuni  4943  coass  5283  fununi  5426  dfmpt3  5483  dfoprab2  6102  dmoprab  6136  rnoprab  6138  mpomptx  6146  resoprab  6151  ovi3  6193  ov6g  6194  oprabex3  6324  xpassen  7083  enq0enq  7751  enq0sym  7752  enq0tr  7754  ltresr  8159  axaddf  8188  axmulf  8189