Theorem 2exbii 1594

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

Syntax hints:   ↔ wb 104  ∃wex 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-ial 1522

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3exbii  1595  19.42vvvv  1901  3exdistr  1903  cbvex4v  1918  ee4anv  1922  ee8anv  1923  sbel2x  1986  2eu4  2107  rexcomf  2628  reean  2634  ceqsex3v  2768  ceqsex4v  2769  ceqsex8v  2771  copsexg  4222  opelopabsbALT  4237  opabm  4258  uniuni  4429  rabxp  4641  elxp3  4658  elvv  4666  elvvv  4667  rexiunxp  4746  elcnv2  4782  cnvuni  4790  coass  5122  fununi  5256  dfmpt3  5310  dfoprab2  5889  dmoprab  5923  rnoprab  5925  mpomptx  5933  resoprab  5938  ovi3  5978  ov6g  5979  oprabex3  6097  xpassen  6796  enq0enq  7372  enq0sym  7373  enq0tr  7375  ltresr  7780  axaddf  7809  axmulf  7810