theorem rlameq2d (_G: wff) {x: nat} (a _v1 _v2: nat x): $ _G -> _v1 = _v2 $ > $ _G -> \. x e. a, _v1 = \. x e. a, _v2 $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqidd | _G -> a = a |
|
2 | hyp _h | _G -> _v1 = _v2 |
|
3 | 1, 2 | rlameqd | _G -> \. x e. a, _v1 = \. x e. a, _v2 |