Theorem aiotajust

Description: Soundness justification theorem for df-aiota . (Contributed by AV, 24-Aug-2022)

	Ref	Expression
Assertion	aiotajust	|- |^| { y | { x | ph } = { y } } = |^| { 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	inteqi	|- |^| { y | { x | ph } = { y } } = |^| { z | { x | ph } = { z } }