Description: Restricted quantifier version of one direction of 19.37v . (The other direction holds iff A is nonempty, see r19.37zv .) (Contributed by NM, 2-Apr-2004) Reduce axiom usage. (Revised by Wolf Lammen, 18-Jun-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | r19.37v | |- ( E. x e. A ( ph -> ps ) -> ( ph -> E. x e. A ps ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | |- ( ph -> ph ) |
|
2 | 1 | ralrimivw | |- ( ph -> A. x e. A ph ) |
3 | r19.35 | |- ( E. x e. A ( ph -> ps ) <-> ( A. x e. A ph -> E. x e. A ps ) ) |
|
4 | 3 | biimpi | |- ( E. x e. A ( ph -> ps ) -> ( A. x e. A ph -> E. x e. A ps ) ) |
5 | 2 4 | syl5 | |- ( E. x e. A ( ph -> ps ) -> ( ph -> E. x e. A ps ) ) |