Theorem elscottn0

Description: If the input class has elements, then the Scott's trick set is not empty. (Contributed by BTernaryTau, 23-Aug-2026)

	Ref	Expression
Assertion	elscottn0	$$⊢A\in B\to ScottB\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		ne0i	$$⊢A\in B\to B\ne \varnothing$$
2		scott0b	$$⊢B=\varnothing \leftrightarrow ScottB=\varnothing$$
3	2	necon3bii	$$⊢B\ne \varnothing \leftrightarrow ScottB\ne \varnothing$$
4	1 3	sylib	$$⊢A\in B\to ScottB\ne \varnothing$$