Description: Specialization for restricted generalization with a nonempty class. (Contributed by Alexander van der Vekens, 6-Sep-2018) Avoid ax-10 , ax-12 . (Revised by Gino Giotto, 28-Jun-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | rspn0 | |- ( A =/= (/) -> ( A. x e. A ph -> ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | n0 | |- ( A =/= (/) <-> E. x x e. A ) |
|
| 2 | df-ral | |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) ) |
|
| 3 | exim | |- ( A. x ( x e. A -> ph ) -> ( E. x x e. A -> E. x ph ) ) |
|
| 4 | ax5e | |- ( E. x ph -> ph ) |
|
| 5 | 3 4 | syl6com | |- ( E. x x e. A -> ( A. x ( x e. A -> ph ) -> ph ) ) |
| 6 | 2 5 | syl5bi | |- ( E. x x e. A -> ( A. x e. A ph -> ph ) ) |
| 7 | 1 6 | sylbi | |- ( A =/= (/) -> ( A. x e. A ph -> ph ) ) |