Metamath Proof Explorer


Theorem csbiegf

Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 11-Nov-2005) (Revised by Mario Carneiro, 13-Oct-2016)

Ref Expression
Hypotheses csbiegf.1 AV_xC
csbiegf.2 x=AB=C
Assertion csbiegf AVA/xB=C

Proof

Step Hyp Ref Expression
1 csbiegf.1 AV_xC
2 csbiegf.2 x=AB=C
3 2 ax-gen xx=AB=C
4 csbiebt AV_xCxx=AB=CA/xB=C
5 1 4 mpdan AVxx=AB=CA/xB=C
6 3 5 mpbii AVA/xB=C