Theorem ex_intro ≪ | index | src | ≫

\ex引入

theorem ex_intro {x: set} (A: wff x): $ A \imp \ex x A $;
StepHypRefExpression
1 fo_imp_inslsto_ex_absrs 
\fo y (y = x \imp A \imp \ex x A) \imp \ex y y = x \imp A \imp \ex x A
2 imp_tran 
(y = x \imp x = y) \imp (x = y \imp A \imp \ex x A) \imp y = x \imp A \imp \ex x A
3 eqs_sym 
y = x \imp x = y
4 2, 3 ax_mp 
(x = y \imp A \imp \ex x A) \imp y = x \imp A \imp \ex x A
5 imp_tran 
((\fo x (x = y \imp A) \imp \ex x A) \imp (A \imp \fo x (x = y \imp A)) \imp A \imp \ex x A) \imp
  (((A \imp \fo x (x = y \imp A)) \imp A \imp \ex x A) \imp (x = y \imp A \imp \fo x (x = y \imp A)) \imp x = y \imp A \imp \ex x A) \imp
  (\fo x (x = y \imp A) \imp \ex x A) \imp
  (x = y \imp A \imp \fo x (x = y \imp A)) \imp
  x = y \imp
  A \imp
  \ex x A
6 imp_introl_imp 
(\fo x (x = y \imp A) \imp \ex x A) \imp (A \imp \fo x (x = y \imp A)) \imp A \imp \ex x A
7 5, 6 ax_mp 
(((A \imp \fo x (x = y \imp A)) \imp A \imp \ex x A) \imp (x = y \imp A \imp \fo x (x = y \imp A)) \imp x = y \imp A \imp \ex x A) \imp
  (\fo x (x = y \imp A) \imp \ex x A) \imp
  (x = y \imp A \imp \fo x (x = y \imp A)) \imp
  x = y \imp
  A \imp
  \ex x A
8 imp_introl_imp 
((A \imp \fo x (x = y \imp A)) \imp A \imp \ex x A) \imp (x = y \imp A \imp \fo x (x = y \imp A)) \imp x = y \imp A \imp \ex x A
9 7, 8 ax_mp 
(\fo x (x = y \imp A) \imp \ex x A) \imp (x = y \imp A \imp \fo x (x = y \imp A)) \imp x = y \imp A \imp \ex x A
10 imp_imp_elimrsl 
(\fo x (x = y \imp A) \imp \ex x x = y \imp \ex x A) \imp \ex x x = y \imp \fo x (x = y \imp A) \imp \ex x A
11 fo_imp_insto_ex 
\fo x (x = y \imp A) \imp \ex x x = y \imp \ex x A
12 10, 11 ax_mp 
\ex x x = y \imp \fo x (x = y \imp A) \imp \ex x A
13 existene 
\ex x x = y
14 12, 13 ax_mp 
\fo x (x = y \imp A) \imp \ex x A
15 9, 14 ax_mp 
(x = y \imp A \imp \fo x (x = y \imp A)) \imp x = y \imp A \imp \ex x A
16 substitution 
x = y \imp A \imp \fo x (x = y \imp A)
17 15, 16 ax_mp 
x = y \imp A \imp \ex x A
18 4, 17 ax_mp 
y = x \imp A \imp \ex x A
19 18 intro_fo 
\fo y (y = x \imp A \imp \ex x A)
20 1, 19 ax_mp 
\ex y y = x \imp A \imp \ex x A
21 existene 
\ex y y = x
22 20, 21 ax_mp 
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)