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	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	cbvcllem	⊢ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ 𝜑 ) } = { 𝑦 ∣ ( 𝑋 ⊆ 𝑦 ∧ 𝜓 ) }

Proof

Step	Hyp	Ref	Expression
1		cbvcllem.y	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2	1	cleq2lem	⊢ ( 𝑥 = 𝑦 → ( ( 𝑋 ⊆ 𝑥 ∧ 𝜑 ) ↔ ( 𝑋 ⊆ 𝑦 ∧ 𝜓 ) ) )
3	2	cbvabv	⊢ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ 𝜑 ) } = { 𝑦 ∣ ( 𝑋 ⊆ 𝑦 ∧ 𝜓 ) }