Description: Obsolete version of dfnul2 as of 23-Sep-2024. (Contributed by NM, 26-Dec-1996) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dfnul2OLD | |- (/) = { x | -. x = x } |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-nul | |- (/) = ( _V \ _V ) |
|
| 2 | df-dif | |- ( _V \ _V ) = { x | ( x e. _V /\ -. x e. _V ) } |
|
| 3 | pm3.24 | |- -. ( x e. _V /\ -. x e. _V ) |
|
| 4 | equid | |- x = x |
|
| 5 | 4 | notnoti | |- -. -. x = x |
| 6 | 3 5 | 2false | |- ( ( x e. _V /\ -. x e. _V ) <-> -. x = x ) |
| 7 | 6 | abbii | |- { x | ( x e. _V /\ -. x e. _V ) } = { x | -. x = x } |
| 8 | 1 2 7 | 3eqtri | |- (/) = { x | -. x = x } |