Theorem subsntheo ≪ | index | src | ≫

theorem subsntheo (A: set) (a: nat): $ subsn A -> (theo A = suc a <-> a e. A) $;

Step	Hyp	Ref	Expression
1		theoid	A == {x \| x = a} <-> theo A = suc a
2		eqeq1	x = a -> (x = a <-> a = a)
3	2	elabe	a e. {x \| x = a} <-> a = a
4		eqid	a = a
5	3, 4	mpbir	a e. {x \| x = a}
6		eleq2	A == {x \| x = a} -> (a e. A <-> a e. {x \| x = a})
7	5, 6	mpbiri	A == {x \| x = a} -> a e. A
8	7	a1i	subsn A -> A == {x \| x = a} -> a e. A
9		anll	subsn A /\ a e. A /\ x e. A -> subsn A
10		anr	subsn A /\ a e. A /\ x e. A -> x e. A
11		anlr	subsn A /\ a e. A /\ x e. A -> a e. A
12	9, 10, 11	subsni	subsn A /\ a e. A /\ x e. A -> x = a
13		anr	subsn A /\ a e. A /\ x = a -> x = a
14	13	eleq1d	subsn A /\ a e. A /\ x = a -> (x e. A <-> a e. A)
15		anlr	subsn A /\ a e. A /\ x = a -> a e. A
16	14, 15	mpbird	subsn A /\ a e. A /\ x = a -> x e. A
17	12, 16	ibida	subsn A /\ a e. A -> (x e. A <-> x = a)
18	17	eqab2d	subsn A /\ a e. A -> A == {x \| x = a}
19	18	exp	subsn A -> a e. A -> A == {x \| x = a}
20	8, 19	ibid	subsn A -> (A == {x \| x = a} <-> a e. A)
21	1, 20	syl5bbr	subsn A -> (theo A = suc a <-> a e. 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)