Theorem n0limd

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

	Ref	Expression
Hypotheses	n0limd.1	|- ( ph -> A =/= (/) )
	n0limd.2	|- ( ( ph /\ x e. A ) -> ps )
Assertion	n0limd	|- ( ph -> ps )

Proof

Step	Hyp	Ref	Expression
1		n0limd.1	|- ( ph -> A =/= (/) )
2		n0limd.2	|- ( ( ph /\ x e. A ) -> ps )
3		n0	|- ( A =/= (/) <-> E. x x e. A )
4	1 3	sylib	|- ( ph -> E. x x e. A )
5	4 2	exlimddv	|- ( ph -> ps )