Theorem sn-iotaval

Description: iotaval without ax-10 , ax-11 , ax-12 . (Contributed by SN, 23-Nov-2024)

	Ref	Expression
Assertion	sn-iotaval	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 𝜑 ) = 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		abbi1sn	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → { 𝑥 ∣ 𝜑 } = { 𝑦 } )
2		iotavallem	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = 𝑦 )
3	1 2	syl	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 𝜑 ) = 𝑦 )