Metamath Proof Explorer

Theorem iotasbc

Description: Definition *14.01 in WhiteheadRussell p. 184. In Principia Mathematica, Russell and Whitehead define iota in terms of a function of ( iota x ph ) . Their definition differs in that a function of ( iota x ph ) evaluates to "false" when there isn't a single x that satisfies ph . (Contributed by Andrew Salmon, 11-Jul-2011)

Ref Expression
Assertion iotasbc ⊢ ∃! x φ → [˙ ι x | φ / y]˙ ψ ↔ ∃ y ∀ x φ ↔ x = y ∧ ψ

Proof

Step Hyp Ref Expression
1 sbc5 ⊢ [˙ ι x | φ / y]˙ ψ ↔ ∃ y y = ι x | φ ∧ ψ
2 iotaexeu ⊢ ∃! x φ → ι x | φ ∈ V
3 eueq ⊢ ι x | φ ∈ V ↔ ∃! y y = ι x | φ
4 2 3 sylib ⊢ ∃! x φ → ∃! y y = ι x | φ
5 eu6 ⊢ ∃! x φ ↔ ∃ y ∀ x φ ↔ x = y
6 iotaval ⊢ ∀ x φ ↔ x = y → ι x | φ = y
7 6 eqcomd ⊢ ∀ x φ ↔ x = y → y = ι x | φ
8 7 ancri ⊢ ∀ x φ ↔ x = y → y = ι x | φ ∧ ∀ x φ ↔ x = y
9 8 eximi ⊢ ∃ y ∀ x φ ↔ x = y → ∃ y y = ι x | φ ∧ ∀ x φ ↔ x = y
10 5 9 sylbi ⊢ ∃! x φ → ∃ y y = ι x | φ ∧ ∀ x φ ↔ x = y
11 eupick ⊢ ∃! y y = ι x | φ ∧ ∃ y y = ι x | φ ∧ ∀ x φ ↔ x = y → y = ι x | φ → ∀ x φ ↔ x = y
12 4 10 11 syl2anc ⊢ ∃! x φ → y = ι x | φ → ∀ x φ ↔ x = y
13 12 7 impbid1 ⊢ ∃! x φ → y = ι x | φ ↔ ∀ x φ ↔ x = y
14 13 anbi1d ⊢ ∃! x φ → y = ι x | φ ∧ ψ ↔ ∀ x φ ↔ x = y ∧ ψ
15 14 exbidv ⊢ ∃! x φ → ∃ y y = ι x | φ ∧ ψ ↔ ∃ y ∀ x φ ↔ x = y ∧ ψ
16 1 15 bitrid ⊢ ∃! x φ → [˙ ι x | φ / y]˙ ψ ↔ ∃ y ∀ x φ ↔ x = y ∧ ψ