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 
|- { y | { x | ph } = { y } } = { z | { y | { x | ph } = { y } } = { z } }

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( { x | ph } = { w } -> ( { x | ph } = { z } <-> { w } = { z } ) )
2 sneqbg 
 |-  ( w e. _V -> ( { w } = { z } <-> w = z ) )
3 2 elv 
 |-  ( { w } = { z } <-> w = z )
4 equcom 
 |-  ( w = z <-> z = w )
5 3 4 bitri 
 |-  ( { w } = { z } <-> z = w )
6 1 5 bitrdi 
 |-  ( { x | ph } = { w } -> ( { x | ph } = { z } <-> z = w ) )
7 sneq 
 |-  ( y = z -> { y } = { z } )
8 7 eqeq2d 
 |-  ( y = z -> ( { x | ph } = { y } <-> { x | ph } = { z } ) )
9 8 elabg 
 |-  ( z e. _V -> ( z e. { y | { x | ph } = { y } } <-> { x | ph } = { z } ) )
10 9 elv 
 |-  ( z e. { y | { x | ph } = { y } } <-> { x | ph } = { z } )
11 velsn 
 |-  ( z e. { w } <-> z = w )
12 6 10 11 3bitr4g 
 |-  ( { x | ph } = { w } -> ( z e. { y | { x | ph } = { y } } <-> z e. { w } ) )
13 12 eqrdv 
 |-  ( { x | ph } = { w } -> { y | { x | ph } = { y } } = { w } )
14 vsnid 
 |-  w e. { w }
15 eleq2 
 |-  ( { y | { x | ph } = { y } } = { w } -> ( w e. { y | { x | ph } = { y } } <-> w e. { w } ) )
16 14 15 mpbiri 
 |-  ( { y | { x | ph } = { y } } = { w } -> w e. { y | { x | ph } = { y } } )
17 sneq 
 |-  ( y = w -> { y } = { w } )
18 17 eqeq2d 
 |-  ( y = w -> ( { x | ph } = { y } <-> { x | ph } = { w } ) )
19 18 elabg 
 |-  ( w e. _V -> ( w e. { y | { x | ph } = { y } } <-> { x | ph } = { w } ) )
20 19 elv 
 |-  ( w e. { y | { x | ph } = { y } } <-> { x | ph } = { w } )
21 16 20 sylib 
 |-  ( { y | { x | ph } = { y } } = { w } -> { x | ph } = { w } )
22 13 21 impbii 
 |-  ( { x | ph } = { w } <-> { y | { x | ph } = { y } } = { w } )
23 sneq 
 |-  ( z = w -> { z } = { w } )
24 23 eqeq2d 
 |-  ( z = w -> ( { y | { x | ph } = { y } } = { z } <-> { y | { x | ph } = { y } } = { w } ) )
25 24 elabg 
 |-  ( w e. _V -> ( w e. { z | { y | { x | ph } = { y } } = { z } } <-> { y | { x | ph } = { y } } = { w } ) )
26 25 elv 
 |-  ( w e. { z | { y | { x | ph } = { y } } = { z } } <-> { y | { x | ph } = { y } } = { w } )
27 22 20 26 3bitr4i 
 |-  ( w e. { y | { x | ph } = { y } } <-> w e. { z | { y | { x | ph } = { y } } = { z } } )
28 27 eqriv 
 |-  { y | { x | ph } = { y } } = { z | { y | { x | ph } = { y } } = { z } }