Theorem eqthe0d ≪ | index | src | ≫

theorem eqthe0d (A: set) (G: wff) {x: nat}:
  $ G -> x e. A -> x = 0 $ >
  $ G -> the A = 0 $;

Step	Hyp	Ref	Expression
1		theid	A == {y \| y = 0} -> the A = 0
2		anr	G /\ A == {y \| y = x} -> A == {y \| y = x}
3		eqeq2	x = 0 -> (y = x <-> y = 0)
4	3	abeqd	x = 0 -> {y \| y = x} == {y \| y = 0}
5		eqeq1	y = x -> (y = x <-> x = x)
6	5	elabe	x e. {y \| y = x} <-> x = x
7		eqid	x = x
8	6, 7	mpbir	x e. {y \| y = x}
9		eleq2	A == {y \| y = x} -> (x e. A <-> x e. {y \| y = x})
10	9	anwr	G /\ A == {y \| y = x} -> (x e. A <-> x e. {y \| y = x})
11	8, 10	mpbiri	G /\ A == {y \| y = x} -> x e. A
12		hyp h	G -> x e. A -> x = 0
13	12	anwl	G /\ A == {y \| y = x} -> x e. A -> x = 0
14	11, 13	mpd	G /\ A == {y \| y = x} -> x = 0
15	4, 14	syl	G /\ A == {y \| y = x} -> {y \| y = x} == {y \| y = 0}
16	2, 15	eqstrd	G /\ A == {y \| y = x} -> A == {y \| y = 0}
17	1, 16	syl	G /\ A == {y \| y = x} -> the A = 0
18	17	eexda	G -> E. x A == {y \| y = x} -> the A = 0
19		the0	~E. x A == {y \| y = x} -> the A = 0
20	19	a1i	G -> ~E. x A == {y \| y = x} -> the A = 0
21	18, 20	casesd	G -> the A = 0

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)