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 | |- ( E. x ph <-> Scott { x | ph } =/= (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | abn0 | |- ( { x | ph } =/= (/) <-> E. x ph ) |
|
| 2 | scott0b | |- ( { x | ph } = (/) <-> Scott { x | ph } = (/) ) |
|
| 3 | 2 | necon3bii | |- ( { x | ph } =/= (/) <-> Scott { x | ph } =/= (/) ) |
| 4 | 1 3 | bitr3i | |- ( E. x ph <-> Scott { x | ph } =/= (/) ) |