Theorem _nf_clos_iff ≪ | index | src | ≫

\nf闭包\iff（不可引用）

theorem _nf_clos_iff {x: set} (A B: wff x):
  $ \nf x A $ >
  $ \nf x B $ >
  $ \nf x (A \iff B) $;

Step	Hyp	Ref	Expression
1		hyp h1	\nf x A
2		hyp h2	\nf x B
3	1, 2	_nf_clos_imp	\nf x (A \imp B)
4	2, 1	_nf_clos_imp	\nf x (B \imp A)
5	3, 4	_nf_clos_and	\nf x ((A \imp B) \and (B \imp A))
6	5	conv iff	\nf x (A \iff B)

Axiom use

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