theorem rlameq1d (_G: wff) {x: nat} (_a1 _a2 v: nat x): $ _G -> _a1 = _a2 $ > $ _G -> \. x e. _a1, v = \. x e. _a2, v $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp _h | _G -> _a1 = _a2 |
|
2 | eqidd | _G -> v = v |
|
3 | 1, 2 | rlameqd | _G -> \. x e. _a1, v = \. x e. _a2, v |