theorem nfnx {x: nat} (a b: nat x): $ a = b $ > $ FN/ x b $ > $ FN/ x a $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqeq2 | a = b -> (y = a <-> y = b) |
|
| 2 | hyp h1 | a = b |
|
| 3 | 1, 2 | ax_mp | y = a <-> y = b |
| 4 | hyp h2 | FN/ x b |
|
| 5 | 4 | nfeq2 | F/ x y = b |
| 6 | 3, 5 | nfx | F/ x y = a |
| 7 | 6 | nfnri | FN/ x a |