Theorem sn-iotaval

Description: Version of iotaval using df-iota instead of dfiota2 . (Contributed by SN, 6-Nov-2024)

	Ref	Expression
Assertion	sn-iotaval	|- ( { x | ph } = { y } -> ( iota x ph ) = y )

Proof

Step	Hyp	Ref	Expression
1		df-iota	|- ( iota x ph ) = U. { w | { x | ph } = { w } }
2		eqeq1	|- ( { x | ph } = { y } -> ( { x | ph } = { w } <-> { y } = { w } ) )
3		sneqbg	|- ( y e. _V -> ( { y } = { w } <-> y = w ) )
4	3	elv	|- ( { y } = { w } <-> y = w )
5		equcom	|- ( y = w <-> w = y )
6	4 5	bitri	|- ( { y } = { w } <-> w = y )
7	2 6	bitrdi	|- ( { x | ph } = { y } -> ( { x | ph } = { w } <-> w = y ) )
8	7	alrimiv	|- ( { x | ph } = { y } -> A. w ( { x | ph } = { w } <-> w = y ) )
9		uniabio	|- ( A. w ( { x | ph } = { w } <-> w = y ) -> U. { w | { x | ph } = { w } } = y )
10	8 9	syl	|- ( { x | ph } = { y } -> U. { w | { x | ph } = { w } } = y )
11	1 10	eqtrid	|- ( { x | ph } = { y } -> ( iota x ph ) = y )