Description: Alternate definition of the empty class/set. (Contributed by BJ, 30-Nov-2019) Avoid ax-8 , df-clel . (Revised by Gino Giotto, 3-Sep-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | dfnul4 | |- (/) = { x | F. } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfnul2 | |- (/) = { x | -. x = x } |
|
2 | equid | |- x = x |
|
3 | 2 | notnoti | |- -. -. x = x |
4 | 3 | bifal | |- ( -. x = x <-> F. ) |
5 | 4 | abbii | |- { x | -. x = x } = { x | F. } |
6 | 1 5 | eqtri | |- (/) = { x | F. } |