Metamath Proof Explorer


Theorem csbeq2dv

Description: Formula-building deduction for class substitution. (Contributed by NM, 10-Nov-2005) (Revised by Mario Carneiro, 1-Sep-2015)

Ref Expression
Hypothesis csbeq2dv.1 ( 𝜑𝐵 = 𝐶 )
Assertion csbeq2dv ( 𝜑 𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥 𝐶 )

Proof

Step Hyp Ref Expression
1 csbeq2dv.1 ( 𝜑𝐵 = 𝐶 )
2 1 eleq2d ( 𝜑 → ( 𝑦𝐵𝑦𝐶 ) )
3 2 sbcbidv ( 𝜑 → ( [ 𝐴 / 𝑥 ] 𝑦𝐵[ 𝐴 / 𝑥 ] 𝑦𝐶 ) )
4 3 abbidv ( 𝜑 → { 𝑦[ 𝐴 / 𝑥 ] 𝑦𝐵 } = { 𝑦[ 𝐴 / 𝑥 ] 𝑦𝐶 } )
5 df-csb 𝐴 / 𝑥 𝐵 = { 𝑦[ 𝐴 / 𝑥 ] 𝑦𝐵 }
6 df-csb 𝐴 / 𝑥 𝐶 = { 𝑦[ 𝐴 / 𝑥 ] 𝑦𝐶 }
7 4 5 6 3eqtr4g ( 𝜑 𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥 𝐶 )