Theorem cvbtrcl

Description: Change of bound variable in class of all transitive relations which are supersets of a relation. (Contributed by RP, 5-May-2020)

	Ref	Expression
Assertion	cvbtrcl	|- { x | ( R C_ x /\ ( x o. x ) C_ x ) } = { y | ( R C_ y /\ ( y o. y ) C_ y ) }

Proof

Step	Hyp	Ref	Expression
1		trcleq2lem	|- ( x = y -> ( ( R C_ x /\ ( x o. x ) C_ x ) <-> ( R C_ y /\ ( y o. y ) C_ y ) ) )
2	1	cbvabv	|- { x | ( R C_ x /\ ( x o. x ) C_ x ) } = { y | ( R C_ y /\ ( y o. y ) C_ y ) }