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