Metamath Proof Explorer


Theorem csbeq1d

Description: Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005)

Ref Expression
Hypothesis csbeq1d.1 φA=B
Assertion csbeq1d φA/xC=B/xC

Proof

Step Hyp Ref Expression
1 csbeq1d.1 φA=B
2 csbeq1 A=BA/xC=B/xC
3 1 2 syl φA/xC=B/xC