Theorem sb_def_dif ≪ | index | src | ≫

对不同变量的$ \sb y x A $的定义方式。

theorem sb_def_dif {x: set} (y: set) (A: wff x):
  $ \sb y x A \iff \fo x (x = y \imp A) $;
StepHypRefExpression
1 iff_tran 
(\sb y x A \iff \ex t t = y \imp \fo x (x = y \imp A)) \imp
  (\ex t t = y \imp \fo x (x = y \imp A) \iff \fo x (x = y \imp A)) \imp
  (\sb y x A \iff \fo x (x = y \imp A))
2 iff_tran 
(\sb y x A \iff \fo t (t = y \imp \fo x (x = y \imp A))) \imp
  (\fo t (t = y \imp \fo x (x = y \imp A)) \iff \ex t t = y \imp \fo x (x = y \imp A)) \imp
  (\sb y x A \iff \ex t t = y \imp \fo x (x = y \imp A))
3 imp_iff_insl 
(t = y \imp (\fo x (x = t \imp A) \iff \fo x (x = y \imp A))) \imp (t = y \imp \fo x (x = t \imp A) \iff t = y \imp \fo x (x = y \imp A))
4 _nf_abs 
\nf x t = y
5 iff_intror_imp 
(x = t \iff x = y) \imp (x = t \imp A \iff x = y \imp A)
6 5 _hyp_null_complete 
t = y \imp (x = t \iff x = y) \imp (x = t \imp A \iff x = y \imp A)
7 eqs_repr 
t = y \imp (x = t \iff x = y)
8 7 _hyp_null_complete 
t = y \imp t = y \imp (x = t \iff x = y)
9 _hyp_null_intro 
t = y \imp t = y
10 8, 9 _hyp_mp 
t = y \imp (x = t \iff x = y)
11 6, 10 _hyp_mp 
t = y \imp (x = t \imp A \iff x = y \imp A)
12 4, 11 _hyp_iff_intro_fo 
t = y \imp (\fo x (x = t \imp A) \iff \fo x (x = y \imp A))
13 3, 12 ax_mp 
t = y \imp \fo x (x = t \imp A) \iff t = y \imp \fo x (x = y \imp A)
14 13 iff_intro_fo 
\fo t (t = y \imp \fo x (x = t \imp A)) \iff \fo t (t = y \imp \fo x (x = y \imp A))
15 14 conv sb 
\sb y x A \iff \fo t (t = y \imp \fo x (x = y \imp A))
16 2, 15 ax_mp 
(\fo t (t = y \imp \fo x (x = y \imp A)) \iff \ex t t = y \imp \fo x (x = y \imp A)) \imp (\sb y x A \iff \ex t t = y \imp \fo x (x = y \imp A))
17 _nf_abs 
\nf t \fo x (x = y \imp A)
18 17 fo_imp_distls_ex_nfrs 
\fo t (t = y \imp \fo x (x = y \imp A)) \iff \ex t t = y \imp \fo x (x = y \imp A)
19 16, 18 ax_mp 
\sb y x A \iff \ex t t = y \imp \fo x (x = y \imp A)
20 1, 19 ax_mp 
(\ex t t = y \imp \fo x (x = y \imp A) \iff \fo x (x = y \imp A)) \imp (\sb y x A \iff \fo x (x = y \imp A))
21 iff_tran 
(\ex t t = y \imp \fo x (x = y \imp A) \iff \true \imp \fo x (x = y \imp A)) \imp
  (\true \imp \fo x (x = y \imp A) \iff \fo x (x = y \imp A)) \imp
  (\ex t t = y \imp \fo x (x = y \imp A) \iff \fo x (x = y \imp A))
22 iff_simintro_imp 
(\ex t t = y \iff \true) \imp (\fo x (x = y \imp A) \iff \fo x (x = y \imp A)) \imp (\ex t t = y \imp \fo x (x = y \imp A) \iff \true \imp \fo x (x = y \imp A))
23 prov_iff_true 
\ex t t = y \imp (\ex t t = y \iff \true)
24 existene 
\ex t t = y
25 23, 24 ax_mp 
\ex t t = y \iff \true
26 22, 25 ax_mp 
(\fo x (x = y \imp A) \iff \fo x (x = y \imp A)) \imp (\ex t t = y \imp \fo x (x = y \imp A) \iff \true \imp \fo x (x = y \imp A))
27 iff_refl 
\fo x (x = y \imp A) \iff \fo x (x = y \imp A)
28 26, 27 ax_mp 
\ex t t = y \imp \fo x (x = y \imp A) \iff \true \imp \fo x (x = y \imp A)
29 21, 28 ax_mp 
(\true \imp \fo x (x = y \imp A) \iff \fo x (x = y \imp A)) \imp (\ex t t = y \imp \fo x (x = y \imp A) \iff \fo x (x = y \imp A))
30 true_imp_wff_iff_wff 
\true \imp \fo x (x = y \imp A) \iff \fo x (x = y \imp A)
31 29, 30 ax_mp 
\ex t t = y \imp \fo x (x = y \imp A) \iff \fo x (x = y \imp A)
32 20, 31 ax_mp 
\sb y x A \iff \fo x (x = y \imp A)

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3, ax_gen, ax_4, ax_5, ax_6, ax_7, ax_12)