Theorem _hyp_fo_alloc_prov ≪ | index | src | ≫

fo_alloc_prov的假设无关形式（不可引用）

theorem _hyp_fo_alloc_prov {x: set} (G A: wff x):
  $ \nf x G $ >
  $ G \imp A $ >
  $ G \imp (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	1	_hyp_null_complete	G \imp (A \imp \fo x A) \imp (\fo x A \imp A) \imp (A \iff \fo x A)
3		introl_imp	\fo x A \imp A \imp \fo x A
4	3	_hyp_null_complete	G \imp \fo x A \imp A \imp \fo x A
5		hyp g	\nf x G
6		hyp h	G \imp A
7	5, 6	_hyp_intro_fo	G \imp \fo x A
8	7	_hyp_null_complete	G \imp G \imp \fo x A
9		_hyp_null_intro	G \imp G
10	8, 9	_hyp_mp	G \imp \fo x A
11	4, 10	_hyp_mp	G \imp A \imp \fo x A
12	2, 11	_hyp_mp	G \imp (\fo x A \imp A) \imp (A \iff \fo x A)
13		fo_elim	\fo x A \imp A
14	13	_hyp_null_complete	G \imp \fo x A \imp A
15	12, 14	_hyp_mp	G \imp (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)