Metamath Proof Explorer

Theorem exellim

Description: Closed form of exellimddv . See also exlimim for a more general theorem. (Contributed by ML, 17-Jul-2020)

Ref Expression
Assertion exellim 
|- ( ( E. x x e. A /\ A. x ( x e. A -> ph ) ) -> ph )

Proof

Step Hyp Ref Expression
1 nfa1 
 |-  F/ x A. x ( x e. A -> ph )
2 nfv 
 |-  F/ x ph
3 sp 
 |-  ( A. x ( x e. A -> ph ) -> ( x e. A -> ph ) )
4 1 2 3 exlimd 
 |-  ( A. x ( x e. A -> ph ) -> ( E. x x e. A -> ph ) )
5 4 impcom 
 |-  ( ( E. x x e. A /\ A. x ( x e. A -> ph ) ) -> ph )