Theorem scott0bs

Description: Theorem scheme version of scott0b . The collection of all x of minimum rank such that ph ( x ) is true, is not empty iff there is an x such that ph ( x ) holds. (Contributed by NM, 13-Oct-2003) Use the Scott operation. (Revised by BTernaryTau, 22-Jul-2026)

	Ref	Expression
Assertion	scott0bs	$$⊢\exists x\phi \leftrightarrow Scott\left\{x|\phi \right\}\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		abn0	$$⊢\left\{x|\phi \right\}\ne \varnothing \leftrightarrow \exists x\phi$$
2		scott0b	$$⊢\left\{x|\phi \right\}=\varnothing \leftrightarrow Scott\left\{x|\phi \right\}=\varnothing$$
3	2	necon3bii	$$⊢\left\{x|\phi \right\}\ne \varnothing \leftrightarrow Scott\left\{x|\phi \right\}\ne \varnothing$$
4	1 3	bitr3i	$$⊢\exists x\phi \leftrightarrow Scott\left\{x|\phi \right\}\ne \varnothing$$