Description: Inference of restricted abstraction subclass from implication. (Contributed by NM, 14-Oct-1999)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ss2rabi.1 | |- ( x e. A -> ( ph -> ps ) ) |
|
Assertion | ss2rabi | |- { x e. A | ph } C_ { x e. A | ps } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ss2rabi.1 | |- ( x e. A -> ( ph -> ps ) ) |
|
2 | ss2rab | |- ( { x e. A | ph } C_ { x e. A | ps } <-> A. x e. A ( ph -> ps ) ) |
|
3 | 2 1 | mprgbir | |- { x e. A | ph } C_ { x e. A | ps } |