Metamath Proof Explorer


Theorem csbied2

Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses csbied2.1 φ A V
csbied2.2 φ A = B
csbied2.3 φ x = B C = D
Assertion csbied2 φ A / x C = D

Proof

Step Hyp Ref Expression
1 csbied2.1 φ A V
2 csbied2.2 φ A = B
3 csbied2.3 φ x = B C = D
4 id x = A x = A
5 4 2 sylan9eqr φ x = A x = B
6 5 3 syldan φ x = A C = D
7 1 6 csbied φ A / x C = D