Description: Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011) (Revised by Steven Nguyen, 28-Jun-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ss2abdv.1 | |- ( ph -> ( ps -> ch ) ) |
|
Assertion | ss2abdv | |- ( ph -> { x | ps } C_ { x | ch } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ss2abdv.1 | |- ( ph -> ( ps -> ch ) ) |
|
2 | 1 | sbimdv | |- ( ph -> ( [ y / x ] ps -> [ y / x ] ch ) ) |
3 | df-clab | |- ( y e. { x | ps } <-> [ y / x ] ps ) |
|
4 | df-clab | |- ( y e. { x | ch } <-> [ y / x ] ch ) |
|
5 | 2 3 4 | 3imtr4g | |- ( ph -> ( y e. { x | ps } -> y e. { x | ch } ) ) |
6 | 5 | ssrdv | |- ( ph -> { x | ps } C_ { x | ch } ) |