Theorem sn-iotauni

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

	Ref	Expression
Assertion	sn-iotauni	$$⊢\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		iotavallem	$$⊢\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		vex	$$⊢y\in \mathrm{V}$$
4	3	unisn	$$⊢\bigcup \left\{y\right\}=y$$
5	2 4	eqtr2di	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\to y=\bigcup \left\{x|\phi \right\}$$
6	1 5	eqtrd	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\to \left(\iota x|\phi \right)=\bigcup \left\{x|\phi \right\}$$
7	6	exlimiv	$$⊢\exists y\left\{x|\phi \right\}=\left\{y\right\}\to \left(\iota x|\phi \right)=\bigcup \left\{x|\phi \right\}$$