Theorem _nf_nf_same ≪ | index | src | ≫

同变元\nf\nf（不可引用）

theorem _nf_nf_same {x: set} (A: wff x): $ \nf x \nf x A $;
StepHypRefExpression
1 _nf_ex_same 
\nf x \ex x A
2 _nf_fo_same 
\nf x \fo x A
3 1, 2 _nf_clos_imp 
\nf x (\ex x A \imp \fo x A)
4 3 conv nf 
\nf x \nf x A

Axiom use

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