Theorem 2exbii 1617

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

Syntax hints:   ↔ wb 105  ∃wex 1503

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-ial 1545

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3exbii  1618  19.42vvvv  1925  3exdistr  1927  cbvex4v  1946  ee4anv  1950  ee8anv  1951  sbel2x  2014  2eu4  2135  rexcomf  2656  reean  2663  ceqsex3v  2802  ceqsex4v  2803  ceqsex8v  2805  copsexg  4273  opelopabsbALT  4289  opabm  4311  uniuni  4482  rabxp  4696  elxp3  4713  elvv  4721  elvvv  4722  rexiunxp  4804  elcnv2  4840  cnvuni  4848  coass  5184  fununi  5322  dfmpt3  5376  dfoprab2  5965  dmoprab  5999  rnoprab  6001  mpomptx  6009  resoprab  6014  ovi3  6055  ov6g  6056  oprabex3  6181  xpassen  6884  enq0enq  7491  enq0sym  7492  enq0tr  7494  ltresr  7899  axaddf  7928  axmulf  7929