Metamath Proof Explorer


Theorem csbeq1a

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

Ref Expression
Assertion csbeq1a ( 𝑥 = 𝐴𝐵 = 𝐴 / 𝑥 𝐵 )

Proof

Step Hyp Ref Expression
1 csbid 𝑥 / 𝑥 𝐵 = 𝐵
2 csbeq1 ( 𝑥 = 𝐴 𝑥 / 𝑥 𝐵 = 𝐴 / 𝑥 𝐵 )
3 1 2 eqtr3id ( 𝑥 = 𝐴𝐵 = 𝐴 / 𝑥 𝐵 )