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	$⊢ (\exists x x \in A \land \forall x (x \in A \to φ)) \to φ$

Step	Hyp	Ref	Expression
1		nfa1	$⊢ Ⅎ x \forall x (x \in A \to φ)$
2		nfv	$⊢ Ⅎ x φ$
3		sp	$⊢ \forall x (x \in A \to φ) \to (x \in A \to φ)$
4	1 2 3	exlimd	$⊢ \forall x (x \in A \to φ) \to (\exists x x \in A \to φ)$
5	4	impcom	$⊢ (\exists x x \in A \land \forall x (x \in A \to φ)) \to φ$