![]() |
Quantum Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > QLE Home > Th. List > df-f | GIF version |
Description: Define false. (Contributed by NM, 9-Aug-1997.) |
Ref | Expression |
---|---|
df-f | 0 = 1⊥ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wf 9 | . 2 term 0 | |
2 | wt 8 | . . 3 term 1 | |
3 | 2 | wn 4 | . 2 term 1⊥ |
4 | 1, 3 | wb 1 | 1 wff 0 = 1⊥ |
Colors of variables: term |
This definition is referenced by: dff2 100 an1 106 an0 108 1b 117 comm0 178 skr0 242 0i1 273 1i1 274 2vwomlem 365 u1lemnana 645 u2lemnana 646 u4lemnana 648 u1lemnab 650 u2lemnab 651 u3lemnab 652 2oath1 826 oa3-6to3 987 lem3.3.4 1053 |
Copyright terms: Public domain | W3C validator |