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 = A -> B = [_ A / x ]_ B )

Proof

Step Hyp Ref Expression
1 csbid 
 |-  [_ x / x ]_ B = B
2 csbeq1 
 |-  ( x = A -> [_ x / x ]_ B = [_ A / x ]_ B )
3 1 2 eqtr3id 
 |-  ( x = A -> B = [_ A / x ]_ B )