Metamath Proof Explorer


Theorem r19.37v

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 ) )

Proof

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 ) )