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	⊢ { 𝑥 ∣ ( 𝑅 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } = { 𝑦 ∣ ( 𝑅 ⊆ 𝑦 ∧ ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ) }

Proof

Step	Hyp	Ref	Expression
1		trcleq2lem	⊢ ( 𝑥 = 𝑦 → ( ( 𝑅 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) ↔ ( 𝑅 ⊆ 𝑦 ∧ ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ) ) )
2	1	cbvabv	⊢ { 𝑥 ∣ ( 𝑅 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } = { 𝑦 ∣ ( 𝑅 ⊆ 𝑦 ∧ ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ) }