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 φ B = C
Assertion csbeq2dv φ A / x B = A / x C

Proof

Step Hyp Ref Expression
1 csbeq2dv.1 φ B = C
2 nfv x φ
3 2 1 csbeq2d φ A / x B = A / x C