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

Metamath Proof Explorer

Theorem iotajust

Description: Soundness justification theorem for df-iota . (Contributed by Andrew Salmon, 29-Jun-2011)

Ref Expression
Assertion iotajust 
|- U. { y | { x | ph } = { y } } = U. { z | { x | ph } = { z } }

Proof

Step Hyp Ref Expression
1 sneq 
 |-  ( y = w -> { y } = { w } )
2 1 eqeq2d 
 |-  ( y = w -> ( { x | ph } = { y } <-> { x | ph } = { w } ) )
3 2 cbvabv 
 |-  { y | { x | ph } = { y } } = { w | { x | ph } = { w } }
4 sneq 
 |-  ( w = z -> { w } = { z } )
5 4 eqeq2d 
 |-  ( w = z -> ( { x | ph } = { w } <-> { x | ph } = { z } ) )
6 5 cbvabv 
 |-  { w | { x | ph } = { w } } = { z | { x | ph } = { z } }
7 3 6 eqtri 
 |-  { y | { x | ph } = { y } } = { z | { x | ph } = { z } }
8 7 unieqi 
 |-  U. { y | { x | ph } = { y } } = U. { z | { x | ph } = { z } }