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 x x A x x A φ φ

Proof

Step Hyp Ref Expression
1 nfa1 x x x A φ
2 nfv x φ
3 sp x x A φ x A φ
4 1 2 3 exlimd x x A φ x x A φ
5 4 impcom x x A x x A φ φ