This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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