Theorem _nf_false ≪ | index | src | ≫

\nf\false（不可引用）

theorem _nf_false {x: set}: $ \nf x \false $;

Step	Hyp	Ref	Expression
1		_nf_true	\nf x \true
2	1	_nf_clos_neg	\nf x \neg \true
3	2	conv false	\nf x \false

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3, ax_gen, ax_4, ax_10)