theorem nfslem {x y: nat} (A: set y) (a: nat x) (B: set x): $ y = a -> A == B $ > $ FN/ x a $ > $ FS/ x B $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqscom | S[a / y] A == B -> B == S[a / y] A |
|
2 | hyp e | y = a -> A == B |
|
3 | 2 | sbse | S[a / y] A == B |
4 | 1, 3 | ax_mp | B == S[a / y] A |
5 | hyp h | FN/ x a |
|
6 | nfsv | FS/ x A |
|
7 | 5, 6 | nfsbsh | FS/ x S[a / y] A |
8 | 4, 7 | nfsx | FS/ x B |