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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-nul | ||
2 | df-dif | ||
3 | pm3.24 | ||
4 | equid | ||
5 | 4 | notnoti | |
6 | 3 5 | 2false | |
7 | 6 | abbii | |
8 | 1 2 7 | 3eqtri |