Theorem iotaval2

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

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

Proof

Step	Hyp	Ref	Expression
1		df-iota	$$⊢\left(\iota x|\phi \right)=\bigcup \left\{w|\left\{x|\phi \right\}=\left\{w\right\}\right\}$$
2		eqeq1	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\to \left(\left\{x|\phi \right\}=\left\{w\right\}\leftrightarrow \left\{y\right\}=\left\{w\right\}\right)$$
3		sneqbg	$$⊢y\in \mathrm{V}\to \left(\left\{y\right\}=\left\{w\right\}\leftrightarrow y=w\right)$$
4	3	elv	$$⊢\left\{y\right\}=\left\{w\right\}\leftrightarrow y=w$$
5		equcom	$$⊢y=w\leftrightarrow w=y$$
6	4 5	bitri	$$⊢\left\{y\right\}=\left\{w\right\}\leftrightarrow w=y$$
7	2 6	bitrdi	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\to \left(\left\{x|\phi \right\}=\left\{w\right\}\leftrightarrow w=y\right)$$
8	7	alrimiv	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\to \forall w\left(\left\{x|\phi \right\}=\left\{w\right\}\leftrightarrow w=y\right)$$
9		uniabio	$$⊢\forall w\left(\left\{x|\phi \right\}=\left\{w\right\}\leftrightarrow w=y\right)\to \bigcup \left\{w|\left\{x|\phi \right\}=\left\{w\right\}\right\}=y$$
10	8 9	syl	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\to \bigcup \left\{w|\left\{x|\phi \right\}=\left\{w\right\}\right\}=y$$
11	1 10	eqtrid	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\to \left(\iota x|\phi \right)=y$$