Theorem sn-iotaval

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

	Ref	Expression
Assertion	sn-iotaval	|- ( A. x ( ph <-> x = y ) -> ( iota x ph ) = y )

Proof

Step	Hyp	Ref	Expression
1		abbi1sn	|- ( A. x ( ph <-> x = y ) -> { x | ph } = { y } )
2		iotavallem	|- ( { x | ph } = { y } -> ( iota x ph ) = y )
3	1 2	syl	|- ( A. x ( ph <-> x = y ) -> ( iota x ph ) = y )