This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iotavalsb

Description: Theorem *14.242 in WhiteheadRussell p. 192. (Contributed by Andrew Salmon, 11-Jul-2011)

Ref Expression
Assertion iotavalsb ⊢ ∀ x φ ↔ x = y → [˙y / z]˙ ψ ↔ [˙ ι x | φ / z]˙ ψ

Proof

Step Hyp Ref Expression
1 19.8a ⊢ ∀ x φ ↔ x = y → ∃ y ∀ x φ ↔ x = y
2 eu6 ⊢ ∃! x φ ↔ ∃ y ∀ x φ ↔ x = y
3 iotavalb ⊢ ∃! x φ → ∀ x φ ↔ x = y ↔ ι x | φ = y
4 dfsbcq ⊢ y = ι x | φ → [˙y / z]˙ ψ ↔ [˙ ι x | φ / z]˙ ψ
5 4 eqcoms ⊢ ι x | φ = y → [˙y / z]˙ ψ ↔ [˙ ι x | φ / z]˙ ψ
6 3 5 biimtrdi ⊢ ∃! x φ → ∀ x φ ↔ x = y → [˙y / z]˙ ψ ↔ [˙ ι x | φ / z]˙ ψ
7 2 6 sylbir ⊢ ∃ y ∀ x φ ↔ x = y → ∀ x φ ↔ x = y → [˙y / z]˙ ψ ↔ [˙ ι x | φ / z]˙ ψ
8 1 7 mpcom ⊢ ∀ x φ ↔ x = y → [˙y / z]˙ ψ ↔ [˙ ι x | φ / z]˙ ψ