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	⊢ ( ∃ 𝑥 𝜑 ↔ Scott { 𝑥 ∣ 𝜑 } ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		abn0	⊢ ( { 𝑥 ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 𝜑 )
2		scott0b	⊢ ( { 𝑥 ∣ 𝜑 } = ∅ ↔ Scott { 𝑥 ∣ 𝜑 } = ∅ )
3	2	necon3bii	⊢ ( { 𝑥 ∣ 𝜑 } ≠ ∅ ↔ Scott { 𝑥 ∣ 𝜑 } ≠ ∅ )
4	1 3	bitr3i	⊢ ( ∃ 𝑥 𝜑 ↔ Scott { 𝑥 ∣ 𝜑 } ≠ ∅ )