Theorem theoid ≪ | index | src | ≫

theorem theoid {x: nat} (A: set) (a: nat):
  $ A == {x | x = a} <-> theo A = suc a $;

Step	Hyp	Ref	Expression
1		theoid1	A == {x \| x = a} -> theo A = suc a
2		sucne0	theo A = suc a -> theo A != 0
3		con1	(~E. a1 A == {x \| x = a1} -> theo A = 0) -> ~theo A = 0 -> E. a1 A == {x \| x = a1}
4	3	conv ne	(~E. a1 A == {x \| x = a1} -> theo A = 0) -> theo A != 0 -> E. a1 A == {x \| x = a1}
5		theo01	~E. a1 A == {x \| x = a1} -> theo A = 0
6	4, 5	ax_mp	theo A != 0 -> E. a1 A == {x \| x = a1}
7	2, 6	rsyl	theo A = suc a -> E. a1 A == {x \| x = a1}
8		anr	theo A = suc a /\ A == {x \| x = a1} -> A == {x \| x = a1}
9		eqeq2	a1 = a -> (x = a1 <-> x = a)
10	9	abeqd	a1 = a -> {x \| x = a1} == {x \| x = a}
11		peano2	suc a1 = suc a <-> a1 = a
12		theoid1	A == {x \| x = a1} -> theo A = suc a1
13	12	anwr	theo A = suc a /\ A == {x \| x = a1} -> theo A = suc a1
14		anl	theo A = suc a /\ A == {x \| x = a1} -> theo A = suc a
15	13, 14	eqtr3d	theo A = suc a /\ A == {x \| x = a1} -> suc a1 = suc a
16	11, 15	sylib	theo A = suc a /\ A == {x \| x = a1} -> a1 = a
17	10, 16	syl	theo A = suc a /\ A == {x \| x = a1} -> {x \| x = a1} == {x \| x = a}
18	8, 17	eqstrd	theo A = suc a /\ A == {x \| x = a1} -> A == {x \| x = a}
19	18	eexda	theo A = suc a -> E. a1 A == {x \| x = a1} -> A == {x \| x = a}
20	7, 19	mpd	theo A = suc a -> A == {x \| x = a}
21	1, 20	ibii	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, the0), axs_peano (peano1, peano2)