Description: Deduction of abstraction subclass from implication. (Contributed by SN, 22-Dec-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ssabdv.1 | |- ( ph -> ( x e. A -> ps ) ) |
|
Assertion | ssabdv | |- ( ph -> A C_ { x | ps } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssabdv.1 | |- ( ph -> ( x e. A -> ps ) ) |
|
2 | abid1 | |- A = { x | x e. A } |
|
3 | 1 | ss2abdv | |- ( ph -> { x | x e. A } C_ { x | ps } ) |
4 | 2 3 | eqsstrid | |- ( ph -> A C_ { x | ps } ) |