This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbvcsbv

Description: Change the bound variable of a proper substitution into a class using implicit substitution. (Contributed by NM, 30-Sep-2008) (Revised by Mario Carneiro, 13-Oct-2016)

Ref Expression
Hypothesis cbvcsbv.1 ⊢ x = y → B = C
Assertion cbvcsbv ⊢ ⦋ A / x⦌ B = ⦋ A / y⦌ C

Proof

Step Hyp Ref Expression
1 cbvcsbv.1 ⊢ x = y → B = C
2 1 eleq2d ⊢ x = y → z ∈ B ↔ z ∈ C
3 2 cbvsbcvw ⊢ [˙A / x]˙ z ∈ B ↔ [˙A / y]˙ z ∈ C
4 3 abbii ⊢ z | [˙A / x]˙ z ∈ B = z | [˙A / y]˙ z ∈ C
5 df-csb ⊢ ⦋ A / x⦌ B = z | [˙A / x]˙ z ∈ B
6 df-csb ⊢ ⦋ A / y⦌ C = z | [˙A / y]˙ z ∈ C
7 4 5 6 3eqtr4i ⊢ ⦋ A / x⦌ B = ⦋ A / y⦌ C