Metamath Proof Explorer


Theorem csbief

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

Ref Expression
Hypotheses csbief.1
|- A e. _V
csbief.2
|- F/_ x C
csbief.3
|- ( x = A -> B = C )
Assertion csbief
|- [_ A / x ]_ B = C

Proof

Step Hyp Ref Expression
1 csbief.1
 |-  A e. _V
2 csbief.2
 |-  F/_ x C
3 csbief.3
 |-  ( x = A -> B = C )
4 2 a1i
 |-  ( A e. _V -> F/_ x C )
5 4 3 csbiegf
 |-  ( A e. _V -> [_ A / x ]_ B = C )
6 1 5 ax-mp
 |-  [_ A / x ]_ B = C