Theorem sb_alloc_nf ≪ | index | src | ≫

如果A与x无关，则A与[t/x]A等价。

theorem sb_alloc_nf {x: set} (y: set) (A: wff x):
  $ \nf x A $ >
  $ A \iff \sb y x A $;

Step	Hyp	Ref	Expression
1		iff_comp	(A \imp \sb y x A) \imp (\sb y x A \imp A) \imp (A \iff \sb y x A)
2		imp_tran	(A \imp \fo x A) \imp (\fo x A \imp \sb y x A) \imp A \imp \sb y x A
3		hyp n	\nf x A
4	3	fo_intro_nf	A \imp \fo x A
5	2, 4	ax_mp	(\fo x A \imp \sb y x A) \imp A \imp \sb y x A
6		fo_elim_sb	\fo x A \imp \sb y x A
7	5, 6	ax_mp	A \imp \sb y x A
8	1, 7	ax_mp	(\sb y x A \imp A) \imp (A \iff \sb y x A)
9		imp_tran	(\sb y x A \imp \ex x A) \imp (\ex x A \imp A) \imp \sb y x A \imp A
10		sb_to_ex	\sb y x A \imp \ex x A
11	9, 10	ax_mp	(\ex x A \imp A) \imp \sb y x A \imp A
12	3	ex_elim_nf	\ex x A \imp A
13	11, 12	ax_mp	\sb y x A \imp A
14	8, 13	ax_mp	A \iff \sb y 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)