theorem nfsx {x: nat} (A B: set x): $ A == B $ > $ FS/ x B $ > $ FS/ x A $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleq2 | A == B -> (y e. A <-> y e. B) |
|
| 2 | hyp h1 | A == B |
|
| 3 | 1, 2 | ax_mp | y e. A <-> y e. B |
| 4 | hyp h2 | FS/ x B |
|
| 5 | 4 | nfel2 | F/ x y e. B |
| 6 | 3, 5 | nfx | F/ x y e. A |
| 7 | 6 | ax_gen | A. y (F/ x y e. A) |
| 8 | 7 | conv nfs | FS/ x A |