Theorem cbvcllem

Description: Change of bound variable in class of supersets of a with a property. (Contributed by RP, 24-Jul-2020)

	Ref	Expression
Hypothesis	cbvcllem.y	|- ( x = y -> ( ph <-> ps ) )
Assertion	cbvcllem	|- { x | ( X C_ x /\ ph ) } = { y | ( X C_ y /\ ps ) }

Proof

Step	Hyp	Ref	Expression
1		cbvcllem.y	|- ( x = y -> ( ph <-> ps ) )
2	1	cleq2lem	|- ( x = y -> ( ( X C_ x /\ ph ) <-> ( X C_ y /\ ps ) ) )
3	2	cbvabv	|- { x | ( X C_ x /\ ph ) } = { y | ( X C_ y /\ ps ) }