Theorem 2exbii 1620

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

Syntax hints:   ↔ wb 105  ∃wex 1506

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-ial 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3exbii  1621  19.42vvvv  1928  3exdistr  1930  cbvex4v  1949  ee4anv  1953  ee8anv  1954  sbel2x  2017  2eu4  2138  rexcomf  2659  reean  2666  ceqsex3v  2806  ceqsex4v  2807  ceqsex8v  2809  copsexg  4278  opelopabsbALT  4294  opabm  4316  uniuni  4487  rabxp  4701  elxp3  4718  elvv  4726  elvvv  4727  rexiunxp  4809  elcnv2  4845  cnvuni  4853  coass  5189  fununi  5327  dfmpt3  5383  dfoprab2  5973  dmoprab  6007  rnoprab  6009  mpomptx  6017  resoprab  6022  ovi3  6064  ov6g  6065  oprabex3  6195  xpassen  6898  enq0enq  7515  enq0sym  7516  enq0tr  7518  ltresr  7923  axaddf  7952  axmulf  7953