Theorem 2exbii 1586

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

Syntax hints:   ↔ wb 104  ∃wex 1469

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-ial 1515

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3exbii  1587  19.42vvvv  1886  3exdistr  1888  cbvex4v  1903  ee4anv  1907  ee8anv  1908  sbel2x  1974  2eu4  2093  rexcomf  2596  reean  2602  ceqsex3v  2731  ceqsex4v  2732  ceqsex8v  2734  copsexg  4174  opelopabsbALT  4189  opabm  4210  uniuni  4380  rabxp  4584  elxp3  4601  elvv  4609  elvvv  4610  rexiunxp  4689  elcnv2  4725  cnvuni  4733  coass  5065  fununi  5199  dfmpt3  5253  dfoprab2  5826  dmoprab  5860  rnoprab  5862  mpomptx  5870  resoprab  5875  ovi3  5915  ov6g  5916  oprabex3  6035  xpassen  6732  enq0enq  7263  enq0sym  7264  enq0tr  7266  ltresr  7671  axaddf  7700  axmulf  7701