Theorem n0limd

Description: Deduction rule for nonempty classes. (Contributed by Thierry Arnoux, 3-Aug-2025)

	Ref	Expression
Hypotheses	n0limd.1	$$⊢\phi \to A\ne \varnothing$$
	n0limd.2	$$⊢\left(\phi \wedge x\in A\right)\to \psi$$
Assertion	n0limd	$$⊢\phi \to \psi$$

Proof

Step	Hyp	Ref	Expression
1		n0limd.1	$$⊢\phi \to A\ne \varnothing$$
2		n0limd.2	$$⊢\left(\phi \wedge x\in A\right)\to \psi$$
3		n0	$$⊢A\ne \varnothing \leftrightarrow \exists xx\in A$$
4	1 3	sylib	$$⊢\phi \to \exists xx\in A$$
5	4 2	exlimddv	$$⊢\phi \to \psi$$