theorem sseld (A B: set) (G: wff) (a: nat): $ G -> A C_ B $ > $ G -> a e. A $ > $ G -> a e. B $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel | A C_ B -> a e. A -> a e. B |
|
2 | hyp h1 | G -> A C_ B |
|
3 | hyp h2 | G -> a e. A |
|
4 | 1, 2, 3 | sylc | G -> a e. B |