Definition df-f 41

Description: Define false.

Assertion

Ref	Expression
df-f	0 = 1⊥

Detailed syntax breakdown of Definition df-f

Step	Hyp	Ref	Expression
1		wf 10	. 2 term  0
2		wt 9	. . 3 term  1
3	2	wn 4	. 2 term  1⊥
4	1, 3	wb 1	1 wff  0 = 1⊥

This definition is referenced by:  dff2 92  an1 98  an0 100  1b 109  comm0 170  skr0 234  0i1 265  1i1 266  2vwomlem 347  u1lemnana 627  u2lemnana 628  u4lemnana 630  u1lemnab 632  u2lemnab 633  u3lemnab 634  2oath1 808  oa3-6to3 967

metamath.org