theorem nfrn {x: nat} (A: set x): $ FS/ x A $ > $ FS/ x Ran A $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp h | FS/ x A |
|
2 | 1 | nfel2 | F/ x a2, a1 e. A |
3 | 2 | nfex | F/ x E. a2 a2, a1 e. A |
4 | 3 | nfab | FS/ x {a1 | E. a2 a2, a1 e. A} |
5 | 4 | conv Ran | FS/ x Ran A |