theorem sbneq1 {x: nat} (a b c: nat x): $ a = b -> N[a / x] c = N[b / x] c $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbeq1 | a = b -> ([a / x] y = c <-> [b / x] y = c) |
|
| 2 | 1 | abeqd | a = b -> {y | [a / x] y = c} == {y | [b / x] y = c} |
| 3 | 2 | theeqd | a = b -> the {y | [a / x] y = c} = the {y | [b / x] y = c} |
| 4 | 3 | conv sbn | a = b -> N[a / x] c = N[b / x] c |