Theorem 2mos 2283

Description: Double "exists at most one", using implicit substitution. (Contributed by NM, 10-Feb-2005.)

Hypothesis

Ref	Expression
2mos.1	⊢ ((x = z ∧ y = w) → (φ ↔ ψ))

Assertion

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

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

Allowed substitution hints:   φ(x,y)   ψ(z,w)

Proof of Theorem 2mos

Step	Hyp	Ref	Expression
1		2mo 2282	. 2 ⊢ (∃z∃w∀x∀y(φ → (x = z ∧ y = w)) ↔ ∀x∀y∀z∀w((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)))
2		nfv 1619	. . . . . . 7 ⊢ Ⅎxψ
3		nfv 1619	. . . . . . . . . 10 ⊢ Ⅎy x = z
4	3	sbrim 2067	. . . . . . . . 9 ⊢ ([w / y](x = z → φ) ↔ (x = z → [w / y]φ))
5		nfv 1619	. . . . . . . . . 10 ⊢ Ⅎy(x = z → ψ)
6		2mos.1	. . . . . . . . . . . 12 ⊢ ((x = z ∧ y = w) → (φ ↔ ψ))
7	6	expcom 424	. . . . . . . . . . 11 ⊢ (y = w → (x = z → (φ ↔ ψ)))
8	7	pm5.74d 238	. . . . . . . . . 10 ⊢ (y = w → ((x = z → φ) ↔ (x = z → ψ)))
9	5, 8	sbie 2038	. . . . . . . . 9 ⊢ ([w / y](x = z → φ) ↔ (x = z → ψ))
10	4, 9	bitr3i 242	. . . . . . . 8 ⊢ ((x = z → [w / y]φ) ↔ (x = z → ψ))
11	10	pm5.74ri 237	. . . . . . 7 ⊢ (x = z → ([w / y]φ ↔ ψ))
12	2, 11	sbie 2038	. . . . . 6 ⊢ ([z / x][w / y]φ ↔ ψ)
13	12	anbi2i 675	. . . . 5 ⊢ ((φ ∧ [z / x][w / y]φ) ↔ (φ ∧ ψ))
14	13	imbi1i 315	. . . 4 ⊢ (((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)) ↔ ((φ ∧ ψ) → (x = z ∧ y = w)))
15	14	2albii 1567	. . 3 ⊢ (∀z∀w((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)) ↔ ∀z∀w((φ ∧ ψ) → (x = z ∧ y = w)))
16	15	2albii 1567	. 2 ⊢ (∀x∀y∀z∀w((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)) ↔ ∀x∀y∀z∀w((φ ∧ ψ) → (x = z ∧ y = w)))
17	1, 16	bitri 240	1 ⊢ (∃z∃w∀x∀y(φ → (x = z ∧ y = w)) ↔ ∀x∀y∀z∀w((φ ∧ ψ) → (x = z ∧ y = w)))

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540  ∃wex 1541   = wceq 1642  [wsb 1648

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  df-sb 1649

This theorem is referenced by: (None)