Description: The set of variables in a substitution is the union, indexed by the variables in the original expression, of the variables in the substitution to that variable. (Contributed by Mario Carneiro, 18-Jul-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mrsubco.s | |
|
mrsubvrs.v | |
||
mrsubvrs.r | |
||
Assertion | mrsubvrs | |