Theorem _nf_clos_ex_difvar ≪ | index | src | ≫

\nf闭包\ex不同变元（不可引用）

theorem _nf_clos_ex_difvar {x y: set} (A: wff x y):
  $ \nf x A $ >
  $ \nf x \ex y A $;
StepHypRefExpression
1 hyp h 
\nf x A
2 1 _nf_clos_neg 
\nf x \neg A
3 2 _nf_clos_fo_difvar 
\nf x \fo y \neg A
4 3 _nf_clos_neg 
\nf x \neg \fo y \neg A
5 4 conv ex 
\nf x \ex y A

Axiom use

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