theorem ssall (A B: set) (l: nat): $ A C_ B -> all A l -> all B l $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel | A C_ B -> a1 e. A -> a1 e. B |
|
2 | 1 | imim2d | A C_ B -> (a1 e. lmems l -> a1 e. A) -> a1 e. lmems l -> a1 e. B |
3 | 2 | alimd | A C_ B -> A. a1 (a1 e. lmems l -> a1 e. A) -> A. a1 (a1 e. lmems l -> a1 e. B) |
4 | 3 | conv all, subset | A C_ B -> all A l -> all B l |