Theorem ex_intro_fo ≪ | index | src | ≫

\ex引入\fo

theorem ex_intro_fo {x: set} (A: wff x): $ \ex x A \imp \fo x \ex x A $;

Step	Hyp	Ref	Expression
1		negfo_intro_fo	\neg \fo x \neg A \imp \fo x \neg \fo x \neg A
2	1	conv ex	\ex x A \imp \fo x \ex x A

Axiom use

Logic (ax_10)