theorem nfin {x: nat} (A B: set x): $ FS/ x A $ > $ FS/ x B $ > $ FS/ x A i^i B $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp h1 | FS/ x A |
|
2 | 1 | nfel2 | F/ x y e. A |
3 | hyp h2 | FS/ x B |
|
4 | 3 | nfel2 | F/ x y e. B |
5 | 2, 4 | nfan | F/ x y e. A /\ y e. B |
6 | 5 | nfab | FS/ x {y | y e. A /\ y e. B} |
7 | 6 | conv Inter | FS/ x A i^i B |