Description: Theorem 19.22 of Margaris p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994) (Proof shortened by Andrew Salmon, 30-May-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | rexim | |- ( A. x e. A ( ph -> ps ) -> ( E. x e. A ph -> E. x e. A ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | con3 | |- ( ( ph -> ps ) -> ( -. ps -> -. ph ) ) |
|
| 2 | 1 | ral2imi | |- ( A. x e. A ( ph -> ps ) -> ( A. x e. A -. ps -> A. x e. A -. ph ) ) |
| 3 | 2 | con3d | |- ( A. x e. A ( ph -> ps ) -> ( -. A. x e. A -. ph -> -. A. x e. A -. ps ) ) |
| 4 | dfrex2 | |- ( E. x e. A ph <-> -. A. x e. A -. ph ) |
|
| 5 | dfrex2 | |- ( E. x e. A ps <-> -. A. x e. A -. ps ) |
|
| 6 | 3 4 5 | 3imtr4g | |- ( A. x e. A ( ph -> ps ) -> ( E. x e. A ph -> E. x e. A ps ) ) |