Description: Inference based on subclass definition. (Contributed by NM, 21-Jun-1993)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ssriv.1 | |- ( x e. A -> x e. B ) |
|
Assertion | ssriv | |- A C_ B |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssriv.1 | |- ( x e. A -> x e. B ) |
|
2 | dfss2 | |- ( A C_ B <-> A. x ( x e. A -> x e. B ) ) |
|
3 | 2 1 | mpgbir | |- A C_ B |