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	⊢ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑧 ∣ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑧 } }

Proof

Step	Hyp	Ref	Expression
1		eqeq1	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑤 } → ( { 𝑥 ∣ 𝜑 } = { 𝑧 } ↔ { 𝑤 } = { 𝑧 } ) )
2		sneqbg	⊢ ( 𝑤 ∈ V → ( { 𝑤 } = { 𝑧 } ↔ 𝑤 = 𝑧 ) )
3	2	elv	⊢ ( { 𝑤 } = { 𝑧 } ↔ 𝑤 = 𝑧 )
4		equcom	⊢ ( 𝑤 = 𝑧 ↔ 𝑧 = 𝑤 )
5	3 4	bitri	⊢ ( { 𝑤 } = { 𝑧 } ↔ 𝑧 = 𝑤 )
6	1 5	bitrdi	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑤 } → ( { 𝑥 ∣ 𝜑 } = { 𝑧 } ↔ 𝑧 = 𝑤 ) )
7		sneq	⊢ ( 𝑦 = 𝑧 → { 𝑦 } = { 𝑧 } )
8	7	eqeq2d	⊢ ( 𝑦 = 𝑧 → ( { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ { 𝑥 ∣ 𝜑 } = { 𝑧 } ) )
9	8	elabg	⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } ↔ { 𝑥 ∣ 𝜑 } = { 𝑧 } ) )
10	9	elv	⊢ ( 𝑧 ∈ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } ↔ { 𝑥 ∣ 𝜑 } = { 𝑧 } )
11		velsn	⊢ ( 𝑧 ∈ { 𝑤 } ↔ 𝑧 = 𝑤 )
12	6 10 11	3bitr4g	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑤 } → ( 𝑧 ∈ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } ↔ 𝑧 ∈ { 𝑤 } ) )
13	12	eqrdv	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑤 } → { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑤 } )
14		vsnid	⊢ 𝑤 ∈ { 𝑤 }
15		eleq2	⊢ ( { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑤 } → ( 𝑤 ∈ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } ↔ 𝑤 ∈ { 𝑤 } ) )
16	14 15	mpbiri	⊢ ( { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑤 } → 𝑤 ∈ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } )
17		sneq	⊢ ( 𝑦 = 𝑤 → { 𝑦 } = { 𝑤 } )
18	17	eqeq2d	⊢ ( 𝑦 = 𝑤 → ( { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ { 𝑥 ∣ 𝜑 } = { 𝑤 } ) )
19	18	elabg	⊢ ( 𝑤 ∈ V → ( 𝑤 ∈ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } ↔ { 𝑥 ∣ 𝜑 } = { 𝑤 } ) )
20	19	elv	⊢ ( 𝑤 ∈ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } ↔ { 𝑥 ∣ 𝜑 } = { 𝑤 } )
21	16 20	sylib	⊢ ( { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑤 } → { 𝑥 ∣ 𝜑 } = { 𝑤 } )
22	13 21	impbii	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑤 } ↔ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑤 } )
23		sneq	⊢ ( 𝑧 = 𝑤 → { 𝑧 } = { 𝑤 } )
24	23	eqeq2d	⊢ ( 𝑧 = 𝑤 → ( { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑧 } ↔ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑤 } ) )
25	24	elabg	⊢ ( 𝑤 ∈ V → ( 𝑤 ∈ { 𝑧 ∣ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑧 } } ↔ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑤 } ) )
26	25	elv	⊢ ( 𝑤 ∈ { 𝑧 ∣ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑧 } } ↔ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑤 } )
27	22 20 26	3bitr4i	⊢ ( 𝑤 ∈ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } ↔ 𝑤 ∈ { 𝑧 ∣ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑧 } } )
28	27	eqriv	⊢ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑧 ∣ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑧 } }