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