Theorem sn-iotauni

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

	Ref	Expression
Assertion	sn-iotauni	|- ( E. y { x | ph } = { y } -> ( iota x ph ) = U. { x | ph } )

Proof

Step	Hyp	Ref	Expression
1		sn-iotaval	|- ( { x | ph } = { y } -> ( iota x ph ) = y )
2		unieq	|- ( { x | ph } = { y } -> U. { x | ph } = U. { y } )
3		vex	|- y e. _V
4	3	unisn	|- U. { y } = y
5	2 4	eqtr2di	|- ( { x | ph } = { y } -> y = U. { x | ph } )
6	1 5	eqtrd	|- ( { x | ph } = { y } -> ( iota x ph ) = U. { x | ph } )
7	6	exlimiv	|- ( E. y { x | ph } = { y } -> ( iota x ph ) = U. { x | ph } )