Theorem sb_to_ex ≪ | index | src | ≫

如果有一个集合实例满足该公式，则存在一个集合满足该公式。

theorem sb_to_ex {x: set} (y: set) (A: wff x): $ \sb y x A \imp \ex x A $;
StepHypRefExpression
1 imp_tran 
(\sb y x A \imp \ex t \fo x (x = t \imp A)) \imp (\ex t \fo x (x = t \imp A) \imp \ex x A) \imp \sb y x A \imp \ex x A
2 imp_imp_elimrsl 
(\sb y x A \imp \ex t t = y \imp \ex t \fo x (x = t \imp A)) \imp \ex t t = y \imp \sb y x A \imp \ex t \fo x (x = t \imp A)
3 fo_imp_insto_ex 
\fo t (t = y \imp \fo x (x = t \imp A)) \imp \ex t t = y \imp \ex t \fo x (x = t \imp A)
4 3 conv sb 
\sb y x A \imp \ex t t = y \imp \ex t \fo x (x = t \imp A)
5 2, 4 ax_mp 
\ex t t = y \imp \sb y x A \imp \ex t \fo x (x = t \imp A)
6 existene 
\ex t t = y
7 5, 6 ax_mp 
\sb y x A \imp \ex t \fo x (x = t \imp A)
8 1, 7 ax_mp 
(\ex t \fo x (x = t \imp A) \imp \ex x A) \imp \sb y x A \imp \ex x A
9 _nf_abs 
\nf t \ex x A
10 imp_imp_elimrsl 
(\fo x (x = t \imp A) \imp \ex x x = t \imp \ex x A) \imp \ex x x = t \imp \fo x (x = t \imp A) \imp \ex x A
11 fo_imp_insto_ex 
\fo x (x = t \imp A) \imp \ex x x = t \imp \ex x A
12 10, 11 ax_mp 
\ex x x = t \imp \fo x (x = t \imp A) \imp \ex x A
13 existene 
\ex x x = t
14 12, 13 ax_mp 
\fo x (x = t \imp A) \imp \ex x A
15 9, 14 imp_introls_ex_nfrs 
\ex t \fo x (x = t \imp A) \imp \ex x A
16 8, 15 ax_mp 
\sb y x A \imp \ex 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)