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