Theorem theoid1 ≪ | index | src | ≫ 

theorem theoid1 {x: nat} (A: set) (a: nat):
  $ A == {x | x = a} -> theo A = suc a $;
StepHypRefExpression
1 anrl 
A == {x | x = a} /\ (a1 = suc a2 /\ a2 e. A) -> a1 = suc a2
2 eqeq1 
x = a2 -> (x = a <-> a2 = a)
3 2 elabe 
a2 e. {x | x = a} <-> a2 = a
4 anl 
A == {x | x = a} /\ (a1 = suc a2 /\ a2 e. A) -> A == {x | x = a}
5 4 eleq2d 
A == {x | x = a} /\ (a1 = suc a2 /\ a2 e. A) -> (a2 e. A <-> a2 e. {x | x = a})
6 anrr 
A == {x | x = a} /\ (a1 = suc a2 /\ a2 e. A) -> a2 e. A
7 5, 6 mpbid 
A == {x | x = a} /\ (a1 = suc a2 /\ a2 e. A) -> a2 e. {x | x = a}
8 3, 7 sylib 
A == {x | x = a} /\ (a1 = suc a2 /\ a2 e. A) -> a2 = a
9 8 suceqd 
A == {x | x = a} /\ (a1 = suc a2 /\ a2 e. A) -> suc a2 = suc a
10 1, 9 eqtrd 
A == {x | x = a} /\ (a1 = suc a2 /\ a2 e. A) -> a1 = suc a
11 10 eexda 
A == {x | x = a} -> E. a2 (a1 = suc a2 /\ a2 e. A) -> a1 = suc a
12 suceq 
a2 = a -> suc a2 = suc a
13 12 eqeq2d 
a2 = a -> (a1 = suc a2 <-> a1 = suc a)
14 eleq1 
a2 = a -> (a2 e. A <-> a e. A)
15 13, 14 aneqd 
a2 = a -> (a1 = suc a2 /\ a2 e. A <-> a1 = suc a /\ a e. A)
16 15 iexe 
a1 = suc a /\ a e. A -> E. a2 (a1 = suc a2 /\ a2 e. A)
17 anr 
A == {x | x = a} /\ a1 = suc a -> a1 = suc a
18 eqeq1 
x = a -> (x = a <-> a = a)
19 18 elabe 
a e. {x | x = a} <-> a = a
20 eqid 
a = a
21 19, 20 mpbir 
a e. {x | x = a}
22 anl 
A == {x | x = a} /\ a1 = suc a -> A == {x | x = a}
23 22 eleq2d 
A == {x | x = a} /\ a1 = suc a -> (a e. A <-> a e. {x | x = a})
24 21, 23 mpbiri 
A == {x | x = a} /\ a1 = suc a -> a e. A
25 16, 17, 24 sylan 
A == {x | x = a} /\ a1 = suc a -> E. a2 (a1 = suc a2 /\ a2 e. A)
26 25 exp 
A == {x | x = a} -> a1 = suc a -> E. a2 (a1 = suc a2 /\ a2 e. A)
27 11, 26 ibid 
A == {x | x = a} -> (E. a2 (a1 = suc a2 /\ a2 e. A) <-> a1 = suc a)
28 27 eqtheabd 
A == {x | x = a} -> the {a1 | E. a2 (a1 = suc a2 /\ a2 e. A)} = suc a
29 28 conv theo 
A == {x | x = a} -> theo A = suc a

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_set (elab, ax_8), axs_the (theid), axs_peano (peano2)