Metamath Proof Explorer


Theorem csbeq1a

Description: Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005)

Ref Expression
Assertion csbeq1a x=AB=A/xB

Proof

Step Hyp Ref Expression
1 csbid x/xB=B
2 csbeq1 x=Ax/xB=A/xB
3 1 2 eqtr3id x=AB=A/xB