Metamath Proof Explorer

Theorem iota4

Description: Theorem *14.22 in WhiteheadRussell p. 190. (Contributed by Andrew Salmon, 12-Jul-2011)

Ref Expression
Assertion iota4 ⊢ ∃! x φ → [˙ ι x | φ / x]˙ φ

Proof

Step Hyp Ref Expression
1 eu6 ⊢ ∃! x φ ↔ ∃ z ∀ x φ ↔ x = z
2 biimpr ⊢ φ ↔ x = z → x = z → φ
3 2 alimi ⊢ ∀ x φ ↔ x = z → ∀ x x = z → φ
4 sb6 ⊢ z x φ ↔ ∀ x x = z → φ
5 3 4 sylibr ⊢ ∀ x φ ↔ x = z → z x φ
6 iotaval ⊢ ∀ x φ ↔ x = z → ι x | φ = z
7 6 eqcomd ⊢ ∀ x φ ↔ x = z → z = ι x | φ
8 dfsbcq2 ⊢ z = ι x | φ → z x φ ↔ [˙ ι x | φ / x]˙ φ
9 7 8 syl ⊢ ∀ x φ ↔ x = z → z x φ ↔ [˙ ι x | φ / x]˙ φ
10 5 9 mpbid ⊢ ∀ x φ ↔ x = z → [˙ ι x | φ / x]˙ φ
11 10 exlimiv ⊢ ∃ z ∀ x φ ↔ x = z → [˙ ι x | φ / x]˙ φ
12 1 11 sylbi ⊢ ∃! x φ → [˙ ι x | φ / x]˙ φ