Theorem fo_alloc_nf ≪ | index | src | ≫

\fo指配(无关)

theorem fo_alloc_nf {x: set} (A: wff x): $ \nf x A $ > $ A \iff \fo x A $;
StepHypRefExpression
1 iff_comp 
(A \imp \fo x A) \imp (\fo x A \imp A) \imp (A \iff \fo x A)
2 hyp n 
\nf x A
3 2 _nf_decomp 
A \imp \fo x A
4 1, 3 ax_mp 
(\fo x A \imp A) \imp (A \iff \fo x A)
5 fo_elim 
\fo x A \imp A
6 4, 5 ax_mp 
A \iff \fo x A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3, ax_gen, ax_4, ax_5, ax_6, ax_7, ax_12)