Theorem sn-iotalem

Description: An unused lemma showing that many equivalences involving df-iota are potentially provable without ax-10 , ax-11 , ax-12 . (Contributed by SN, 6-Nov-2024)

	Ref	Expression
Assertion	sn-iotalem	$$⊢\left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}=\left\{z|\left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}=\left\{z\right\}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$$⊢\left\{x|\phi \right\}=\left\{w\right\}\to \left(\left\{x|\phi \right\}=\left\{z\right\}\leftrightarrow \left\{w\right\}=\left\{z\right\}\right)$$
2		sneqbg	$$⊢w\in \mathrm{V}\to \left(\left\{w\right\}=\left\{z\right\}\leftrightarrow w=z\right)$$
3	2	elv	$$⊢\left\{w\right\}=\left\{z\right\}\leftrightarrow w=z$$
4		equcom	$$⊢w=z\leftrightarrow z=w$$
5	3 4	bitri	$$⊢\left\{w\right\}=\left\{z\right\}\leftrightarrow z=w$$
6	1 5	bitrdi	$$⊢\left\{x|\phi \right\}=\left\{w\right\}\to \left(\left\{x|\phi \right\}=\left\{z\right\}\leftrightarrow z=w\right)$$
7		sneq	$$⊢y=z\to \left\{y\right\}=\left\{z\right\}$$
8	7	eqeq2d	$$⊢y=z\to \left(\left\{x|\phi \right\}=\left\{y\right\}\leftrightarrow \left\{x|\phi \right\}=\left\{z\right\}\right)$$
9	8	elabg	$$⊢z\in \mathrm{V}\to \left(z\in \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}\leftrightarrow \left\{x|\phi \right\}=\left\{z\right\}\right)$$
10	9	elv	$$⊢z\in \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}\leftrightarrow \left\{x|\phi \right\}=\left\{z\right\}$$
11		velsn	$$⊢z\in \left\{w\right\}\leftrightarrow z=w$$
12	6 10 11	3bitr4g	$$⊢\left\{x|\phi \right\}=\left\{w\right\}\to \left(z\in \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}\leftrightarrow z\in \left\{w\right\}\right)$$
13	12	eqrdv	$$⊢\left\{x|\phi \right\}=\left\{w\right\}\to \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}=\left\{w\right\}$$
14		vsnid	$$⊢w\in \left\{w\right\}$$
15		eleq2	$$⊢\left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}=\left\{w\right\}\to \left(w\in \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}\leftrightarrow w\in \left\{w\right\}\right)$$
16	14 15	mpbiri	$$⊢\left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}=\left\{w\right\}\to w\in \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}$$
17		sneq	$$⊢y=w\to \left\{y\right\}=\left\{w\right\}$$
18	17	eqeq2d	$$⊢y=w\to \left(\left\{x|\phi \right\}=\left\{y\right\}\leftrightarrow \left\{x|\phi \right\}=\left\{w\right\}\right)$$
19	18	elabg	$$⊢w\in \mathrm{V}\to \left(w\in \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}\leftrightarrow \left\{x|\phi \right\}=\left\{w\right\}\right)$$
20	19	elv	$$⊢w\in \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}\leftrightarrow \left\{x|\phi \right\}=\left\{w\right\}$$
21	16 20	sylib	$$⊢\left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}=\left\{w\right\}\to \left\{x|\phi \right\}=\left\{w\right\}$$
22	13 21	impbii	$$⊢\left\{x|\phi \right\}=\left\{w\right\}\leftrightarrow \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}=\left\{w\right\}$$
23		sneq	$$⊢z=w\to \left\{z\right\}=\left\{w\right\}$$
24	23	eqeq2d	$$⊢z=w\to \left(\left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}=\left\{z\right\}\leftrightarrow \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}=\left\{w\right\}\right)$$
25	24	elabg	$$⊢w\in \mathrm{V}\to \left(w\in \left\{z|\left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}=\left\{z\right\}\right\}\leftrightarrow \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}=\left\{w\right\}\right)$$
26	25	elv	$$⊢w\in \left\{z|\left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}=\left\{z\right\}\right\}\leftrightarrow \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}=\left\{w\right\}$$
27	22 20 26	3bitr4i	$$⊢w\in \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}\leftrightarrow w\in \left\{z|\left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}=\left\{z\right\}\right\}$$
28	27	eqriv	$$⊢\left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}=\left\{z|\left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}=\left\{z\right\}\right\}$$