Theorem sn-iotalemcor

Description: Corollary of sn-iotalem . Compare sb8iota . (Contributed by SN, 6-Nov-2024)

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

Proof

Step	Hyp	Ref	Expression
1		sn-iotalem	|- { y | { x | ph } = { y } } = { z | { y | { x | ph } = { y } } = { z } }
2	1	unieqi	|- U. { y | { x | ph } = { y } } = U. { z | { y | { x | ph } = { y } } = { z } }
3		df-iota	|- ( iota x ph ) = U. { y | { x | ph } = { y } }
4		df-iota	|- ( iota y { x | ph } = { y } ) = U. { z | { y | { x | ph } = { y } } = { z } }
5	2 3 4	3eqtr4i	|- ( iota x ph ) = ( iota y { x | ph } = { y } )