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  2803  ceqsex4v  2804  ceqsex8v  2806  copsexg  4274  opelopabsbALT  4290  opabm  4312  uniuni  4483  rabxp  4697  elxp3  4714  elvv  4722  elvvv  4723  rexiunxp  4805  elcnv2  4841  cnvuni  4849  coass  5185  fununi  5323  dfmpt3  5377  dfoprab2  5966  dmoprab  6000  rnoprab  6002  mpomptx  6010  resoprab  6015  ovi3  6057  ov6g  6058  oprabex3  6183  xpassen  6886  enq0enq  7493  enq0sym  7494  enq0tr  7496  ltresr  7901  axaddf  7930  axmulf  7931