Theorem iotauni2

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

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

Proof

Step	Hyp	Ref	Expression
1		iotaval2	|- ( { x | ph } = { y } -> ( iota x ph ) = y )
2		unieq	|- ( { x | ph } = { y } -> U. { x | ph } = U. { y } )
3		unisnv	|- U. { y } = y
4	2 3	eqtr2di	|- ( { x | ph } = { y } -> y = U. { x | ph } )
5	1 4	eqtrd	|- ( { x | ph } = { y } -> ( iota x ph ) = U. { x | ph } )
6	5	exlimiv	|- ( E. y { x | ph } = { y } -> ( iota x ph ) = U. { x | ph } )