Theorem exsuc ≪ | index | src | ≫ 

theorem exsuc {x: nat} (a: nat): $ a != 0 <-> E. x a = suc x $;
StepHypRefExpression
1 eqeq1 
y = a -> (y = 0 <-> a = 0)
2 1 noteqd 
y = a -> (~y = 0 <-> ~a = 0)
3 2 conv ne 
y = a -> (y != 0 <-> a != 0)
4 eqeq1 
y = a -> (y = suc x <-> a = suc x)
5 4 exeqd 
y = a -> (E. x y = suc x <-> E. x a = suc x)
6 3, 5 imeqd 
y = a -> (y != 0 -> E. x y = suc x <-> a != 0 -> E. x a = suc x)
7 eqeq1 
y = 0 -> (y = 0 <-> 0 = 0)
8 7 noteqd 
y = 0 -> (~y = 0 <-> ~0 = 0)
9 8 conv ne 
y = 0 -> (y != 0 <-> ~0 = 0)
10 eqeq1 
y = 0 -> (y = suc x <-> 0 = suc x)
11 10 exeqd 
y = 0 -> (E. x y = suc x <-> E. x 0 = suc x)
12 9, 11 imeqd 
y = 0 -> (y != 0 -> E. x y = suc x <-> ~0 = 0 -> E. x 0 = suc x)
13 eqeq1 
y = z -> (y = 0 <-> z = 0)
14 13 noteqd 
y = z -> (~y = 0 <-> ~z = 0)
15 14 conv ne 
y = z -> (y != 0 <-> ~z = 0)
16 eqeq1 
y = z -> (y = suc x <-> z = suc x)
17 16 exeqd 
y = z -> (E. x y = suc x <-> E. x z = suc x)
18 15, 17 imeqd 
y = z -> (y != 0 -> E. x y = suc x <-> ~z = 0 -> E. x z = suc x)
19 eqeq1 
y = suc z -> (y = 0 <-> suc z = 0)
20 19 noteqd 
y = suc z -> (~y = 0 <-> ~suc z = 0)
21 20 conv ne 
y = suc z -> (y != 0 <-> ~suc z = 0)
22 eqeq1 
y = suc z -> (y = suc x <-> suc z = suc x)
23 22 exeqd 
y = suc z -> (E. x y = suc x <-> E. x suc z = suc x)
24 21, 23 imeqd 
y = suc z -> (y != 0 -> E. x y = suc x <-> ~suc z = 0 -> E. x suc z = suc x)
25 absurdr 
0 = 0 -> ~0 = 0 -> E. x 0 = suc x
26 eqid 
0 = 0
27 25, 26 ax_mp 
~0 = 0 -> E. x 0 = suc x
28 suceq 
x = z -> suc x = suc z
29 28 eqeq2d 
x = z -> (suc z = suc x <-> suc z = suc z)
30 29 iexe 
suc z = suc z -> E. x suc z = suc x
31 eqid 
suc z = suc z
32 30, 31 ax_mp 
E. x suc z = suc x
33 32 a1i 
~suc z = 0 -> E. x suc z = suc x
34 33 a1i 
(~z = 0 -> E. x z = suc x) -> ~suc z = 0 -> E. x suc z = suc x
35 6, 12, 18, 24, 27, 34 ind 
a != 0 -> E. x a = suc x
36 sucne0 
a = suc x -> a != 0
37 36 eex 
E. x a = suc x -> a != 0
38 35, 37 ibii 
a != 0 <-> E. x a = suc x

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_peano (peano1, peano2, peano5)