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 } }