Description: Obsolete version of rspn0 as of 28-Jun-2024. (Contributed by Alexander van der Vekens, 6-Sep-2018) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | rspn0OLD | |- ( A =/= (/) -> ( A. x e. A ph -> ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | n0 | |- ( A =/= (/) <-> E. x x e. A ) |
|
| 2 | nfra1 | |- F/ x A. x e. A ph |
|
| 3 | nfv | |- F/ x ph |
|
| 4 | 2 3 | nfim | |- F/ x ( A. x e. A ph -> ph ) |
| 5 | rsp | |- ( A. x e. A ph -> ( x e. A -> ph ) ) |
|
| 6 | 5 | com12 | |- ( x e. A -> ( A. x e. A ph -> ph ) ) |
| 7 | 4 6 | exlimi | |- ( E. x x e. A -> ( A. x e. A ph -> ph ) ) |
| 8 | 1 7 | sylbi | |- ( A =/= (/) -> ( A. x e. A ph -> ph ) ) |