theorem ssel (A B: set) (a: nat): $ A C_ B -> a e. A -> a e. B $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 | x = a -> (x e. A <-> a e. A) |
|
2 | eleq1 | x = a -> (x e. B <-> a e. B) |
|
3 | 1, 2 | imeqd | x = a -> (x e. A -> x e. B <-> a e. A -> a e. B) |
4 | 3 | eale | A. x (x e. A -> x e. B) -> a e. A -> a e. B |
5 | 4 | conv subset | A C_ B -> a e. A -> a e. B |