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	⊢ ( 𝐴 ∈ 𝐵 → Scott 𝐵 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		ne0i	⊢ ( 𝐴 ∈ 𝐵 → 𝐵 ≠ ∅ )
2		scott0b	⊢ ( 𝐵 = ∅ ↔ Scott 𝐵 = ∅ )
3	2	necon3bii	⊢ ( 𝐵 ≠ ∅ ↔ Scott 𝐵 ≠ ∅ )
4	1 3	sylib	⊢ ( 𝐴 ∈ 𝐵 → Scott 𝐵 ≠ ∅ )