Theorem 2exbii 1659

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

Syntax hints:   ↔ wb 105  ∃wex 1545

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-ial 1587

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3exbii  1660  19.42vvvv  1969  3exdistr  1971  cbvex4v  1990  ee4anv  1994  ee8anv  1995  sbel2x  2058  2eu4  2180  rexcomf  2713  reean  2720  ceqsex3v  2865  ceqsex4v  2866  ceqsex8v  2868  copsexg  4382  opelopabsbALT  4399  opabm  4421  uniuni  4595  rabxp  4810  elxp3  4827  elvv  4835  elvvv  4836  rexiunxp  4920  elcnv2  4956  cnvuni  4964  coass  5304  fununi  5447  dfmpt3  5504  dfoprab2  6129  dmoprab  6163  rnoprab  6165  mpomptx  6173  resoprab  6178  ovi3  6220  ov6g  6221  oprabex3  6356  xpassen  7122  enq0enq  7792  enq0sym  7793  enq0tr  7795  ltresr  8200  axaddf  8229  axmulf  8230