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 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( [ 𝑦 / 𝑧 ] 𝜓 ↔ [ ( ℩ 𝑥 𝜑 ) / 𝑧 ] 𝜓 ) )

Proof

Step Hyp Ref Expression
1 19.8a ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) )
2 eu6 ⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) )
3 iotavalb ⊢ ( ∃! 𝑥 𝜑 → ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ( ℩ 𝑥 𝜑 ) = 𝑦 ) )
4 dfsbcq ⊢ ( 𝑦 = ( ℩ 𝑥 𝜑 ) → ( [ 𝑦 / 𝑧 ] 𝜓 ↔ [ ( ℩ 𝑥 𝜑 ) / 𝑧 ] 𝜓 ) )
5 4 eqcoms ⊢ ( ( ℩ 𝑥 𝜑 ) = 𝑦 → ( [ 𝑦 / 𝑧 ] 𝜓 ↔ [ ( ℩ 𝑥 𝜑 ) / 𝑧 ] 𝜓 ) )
6 3 5 biimtrdi ⊢ ( ∃! 𝑥 𝜑 → ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( [ 𝑦 / 𝑧 ] 𝜓 ↔ [ ( ℩ 𝑥 𝜑 ) / 𝑧 ] 𝜓 ) ) )
7 2 6 sylbir ⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( [ 𝑦 / 𝑧 ] 𝜓 ↔ [ ( ℩ 𝑥 𝜑 ) / 𝑧 ] 𝜓 ) ) )
8 1 7 mpcom ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( [ 𝑦 / 𝑧 ] 𝜓 ↔ [ ( ℩ 𝑥 𝜑 ) / 𝑧 ] 𝜓 ) )