Theorem iotauni2

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

	Ref	Expression
Assertion	iotauni2	$$⊢\exists y\left\{x|\phi \right\}=\left\{y\right\}\to \left(\iota x|\phi \right)=\bigcup \left\{x|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		iotaval2	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\to \left(\iota x|\phi \right)=y$$
2		unieq	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\to \bigcup \left\{x|\phi \right\}=\bigcup \left\{y\right\}$$
3		unisnv	$$⊢\bigcup \left\{y\right\}=y$$
4	2 3	eqtr2di	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\to y=\bigcup \left\{x|\phi \right\}$$
5	1 4	eqtrd	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\to \left(\iota x|\phi \right)=\bigcup \left\{x|\phi \right\}$$
6	5	exlimiv	$$⊢\exists y\left\{x|\phi \right\}=\left\{y\right\}\to \left(\iota x|\phi \right)=\bigcup \left\{x|\phi \right\}$$