Theorem fo_alloc_prov ≪ | index | src | ≫

\fo指配(可证)

theorem fo_alloc_prov {x: set} (A: wff x): $ A $ > $ A \iff \fo x A $;

Step	Hyp	Ref	Expression
1		iff_comp	(A \imp \fo x A) \imp (\fo x A \imp A) \imp (A \iff \fo x A)
2		introl_imp	\fo x A \imp A \imp \fo x A
3		hyp h	A
4	3	intro_fo	\fo x A
5	2, 4	ax_mp	A \imp \fo x A
6	1, 5	ax_mp	(\fo x A \imp A) \imp (A \iff \fo x A)
7		fo_elim	\fo x A \imp A
8	6, 7	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)