Metamath Proof Explorer


Theorem csbconstgi

Description: The proper substitution of a class for a variable in another variable does not modify it, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019)

Ref Expression
Hypothesis csbconstgi.1 AV
Assertion csbconstgi A/xy=y

Proof

Step Hyp Ref Expression
1 csbconstgi.1 AV
2 csbconstg AVA/xy=y
3 1 2 ax-mp A/xy=y