Theorem iff_intro_nf ≪ | index | src | ≫

\iff引入\nf（不可引用）

theorem iff_intro_nf {x: set} (A B: wff x):
  $ A \iff B $ >
  $ \nf x A \iff \nf x B $;
StepHypRefExpression
1 iff_simintro_imp 
(\ex x A \iff \ex x B) \imp (\fo x A \iff \fo x B) \imp (\ex x A \imp \fo x A \iff \ex x B \imp \fo x B)
2 hyp h 
A \iff B
3 2 iff_intro_ex 
\ex x A \iff \ex x B
4 1, 3 ax_mp 
(\fo x A \iff \fo x B) \imp (\ex x A \imp \fo x A \iff \ex x B \imp \fo x B)
5 2 iff_intro_fo 
\fo x A \iff \fo x B
6 4, 5 ax_mp 
\ex x A \imp \fo x A \iff \ex x B \imp \fo x B
7 6 conv nf 
\nf x A \iff \nf x B

Axiom use

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