Theorem 2exsb 2132

Description: An equivalent expression for double existence. (Contributed by NM, 2-Feb-2005.)

Assertion

Ref	Expression
2exsb	⊢ (∃x∃yφ ↔ ∃z∃w∀x∀y((x = z ∧ y = w) → φ))

Distinct variable groups:   x,y,z   y,w,z   φ,z,w

Allowed substitution hints:   φ(x,y)

Proof of Theorem 2exsb

Step	Hyp	Ref	Expression
1		exsb 2130	. . . 4 ⊢ (∃yφ ↔ ∃w∀y(y = w → φ))
2	1	exbii 1582	. . 3 ⊢ (∃x∃yφ ↔ ∃x∃w∀y(y = w → φ))
3		excom 1741	. . 3 ⊢ (∃x∃w∀y(y = w → φ) ↔ ∃w∃x∀y(y = w → φ))
4	2, 3	bitri 240	. 2 ⊢ (∃x∃yφ ↔ ∃w∃x∀y(y = w → φ))
5		exsb 2130	. . . . 5 ⊢ (∃x∀y(y = w → φ) ↔ ∃z∀x(x = z → ∀y(y = w → φ)))
6		impexp 433	. . . . . . . . 9 ⊢ (((x = z ∧ y = w) → φ) ↔ (x = z → (y = w → φ)))
7	6	albii 1566	. . . . . . . 8 ⊢ (∀y((x = z ∧ y = w) → φ) ↔ ∀y(x = z → (y = w → φ)))
8		19.21v 1890	. . . . . . . 8 ⊢ (∀y(x = z → (y = w → φ)) ↔ (x = z → ∀y(y = w → φ)))
9	7, 8	bitr2i 241	. . . . . . 7 ⊢ ((x = z → ∀y(y = w → φ)) ↔ ∀y((x = z ∧ y = w) → φ))
10	9	albii 1566	. . . . . 6 ⊢ (∀x(x = z → ∀y(y = w → φ)) ↔ ∀x∀y((x = z ∧ y = w) → φ))
11	10	exbii 1582	. . . . 5 ⊢ (∃z∀x(x = z → ∀y(y = w → φ)) ↔ ∃z∀x∀y((x = z ∧ y = w) → φ))
12	5, 11	bitri 240	. . . 4 ⊢ (∃x∀y(y = w → φ) ↔ ∃z∀x∀y((x = z ∧ y = w) → φ))
13	12	exbii 1582	. . 3 ⊢ (∃w∃x∀y(y = w → φ) ↔ ∃w∃z∀x∀y((x = z ∧ y = w) → φ))
14		excom 1741	. . 3 ⊢ (∃w∃z∀x∀y((x = z ∧ y = w) → φ) ↔ ∃z∃w∀x∀y((x = z ∧ y = w) → φ))
15	13, 14	bitri 240	. 2 ⊢ (∃w∃x∀y(y = w → φ) ↔ ∃z∃w∀x∀y((x = z ∧ y = w) → φ))
16	4, 15	bitri 240	1 ⊢ (∃x∃yφ ↔ ∃z∃w∀x∀y((x = z ∧ y = w) → φ))

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545

This theorem is referenced by:  2eu6  2289