theorem nfres {x: nat} (A B: set x): $ FS/ x A $ > $ FS/ x B $ > $ FS/ x A |` B $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp h1 | FS/ x A |
|
2 | hyp h2 | FS/ x B |
|
3 | nfsv | FS/ x _V |
|
4 | 2, 3 | nfxp | FS/ x Xp B _V |
5 | 1, 4 | nfin | FS/ x A i^i Xp B _V |
6 | 5 | conv res | FS/ x A |` B |