Description: Theorem 19.2 of Margaris p. 89 with restricted quantifiers (compare 19.2 ). The restricted version is valid only when the domain of quantification is not empty. (Contributed by NM, 15-Nov-2003)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | r19.2z | |- ( ( A =/= (/) /\ A. x e. A ph ) -> E. x e. A ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-ral | |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) ) |
|
| 2 | exintr | |- ( A. x ( x e. A -> ph ) -> ( E. x x e. A -> E. x ( x e. A /\ ph ) ) ) |
|
| 3 | 1 2 | sylbi | |- ( A. x e. A ph -> ( E. x x e. A -> E. x ( x e. A /\ ph ) ) ) |
| 4 | n0 | |- ( A =/= (/) <-> E. x x e. A ) |
|
| 5 | df-rex | |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) ) |
|
| 6 | 3 4 5 | 3imtr4g | |- ( A. x e. A ph -> ( A =/= (/) -> E. x e. A ph ) ) |
| 7 | 6 | impcom | |- ( ( A =/= (/) /\ A. x e. A ph ) -> E. x e. A ph ) |