theorem nfnbid (G: wff) {x: nat} (a b: nat x):
$ G -> a = b $ >
$ G -> ((FN/ x a) <-> (FN/ x b)) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hyp h | G -> a = b |
|
| 2 | 1 | eqeq2d | G -> (y = a <-> y = b) |
| 3 | 2 | nfeqd | G -> ((F/ x y = a) <-> (F/ x y = b)) |
| 4 | 3 | aleqd | G -> (A. y (F/ x y = a) <-> A. y (F/ x y = b)) |
| 5 | 4 | conv nfn | G -> ((FN/ x a) <-> (FN/ x b)) |