Theorem iotaequ

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

	Ref	Expression
Assertion	iotaequ	⊢ ( ℩ 𝑥 𝑥 = 𝑦 ) = 𝑦

Proof

Step	Hyp	Ref	Expression
1		iotaval	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 𝑥 = 𝑦 ) = 𝑦 )
2		biid	⊢ ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑦 )
3	1 2	mpg	⊢ ( ℩ 𝑥 𝑥 = 𝑦 ) = 𝑦