Metamath Proof Explorer
Description: Formulabuilding deduction for class substitution. (Contributed by NM, 10Nov2005) (Revised by Mario Carneiro, 1Sep2015)


Ref 
Expression 

Hypothesis 
csbeq2dv.1 
$${\u22a2}{\phi}\to {B}={C}$$ 

Assertion 
csbeq2dv 
$${\u22a2}{\phi}\to \u298b{A}/{x}\u298c{B}=\u298b{A}/{x}\u298c{C}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

csbeq2dv.1 
$${\u22a2}{\phi}\to {B}={C}$$ 
2 

nfv 
$${\u22a2}\u2132{x}\phantom{\rule{.4em}{0ex}}{\phi}$$ 
3 
2 1

csbeq2d 
$${\u22a2}{\phi}\to \u298b{A}/{x}\u298c{B}=\u298b{A}/{x}\u298c{C}$$ 