Theorem 2exbii 1497

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

Syntax hints:   ↔ wb 98  ∃wex 1381

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-ial 1427

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  3exbii  1498  19.42vvvv  1790  3exdistr  1792  cbvex4v  1805  ee4anv  1809  ee8anv  1810  sbel2x  1874  2eu4  1993  rexcomf  2472  reean  2478  ceqsex3v  2596  ceqsex4v  2597  ceqsex8v  2599  copsexg  3981  opelopabsbALT  3996  opabm  4017  uniuni  4183  rabxp  4380  elxp3  4394  elvv  4402  elvvv  4403  rexiunxp  4478  elcnv2  4513  cnvuni  4521  coass  4839  fununi  4967  dfmpt3  5021  dfoprab2  5552  dmoprab  5585  rnoprab  5587  mpt2mptx  5595  resoprab  5597  ovi3  5637  ov6g  5638  oprabex3  5756  xpassen  6304  enq0enq  6529  enq0sym  6530  enq0tr  6532  ltresr  6915