Theorem eqtheb ≪ | index | src | ≫

theorem eqtheb (A: set) (a: nat) {x y: nat}:
  $ a = the A <-> A == {x | x = a} \/ ~E. y A == {x | x = y} /\ a = 0 $;

Step	Hyp	Ref	Expression
1		nfv	F/ y a = the A
2		nfv	F/ y A == {x \| x = a}
3		nfex1	F/ y E. y A == {x \| x = y}
4	3	nfnot	F/ y ~E. y A == {x \| x = y}
5		nfv	F/ y a = 0
6	4, 5	nfan	F/ y ~E. y A == {x \| x = y} /\ a = 0
7	2, 6	nfor	F/ y A == {x \| x = a} \/ ~E. y A == {x \| x = y} /\ a = 0
8		eqeq2	a = y -> (x = a <-> x = y)
9	8	abeqd	a = y -> {x \| x = a} == {x \| x = y}
10	9	eqseq2d	a = y -> (A == {x \| x = a} <-> A == {x \| x = y})
11		anl	a = the A /\ A == {x \| x = y} -> a = the A
12		theid	A == {x \| x = y} -> the A = y
13	12	anwr	a = the A /\ A == {x \| x = y} -> the A = y
14	11, 13	eqtrd	a = the A /\ A == {x \| x = y} -> a = y
15	10, 14	syl	a = the A /\ A == {x \| x = y} -> (A == {x \| x = a} <-> A == {x \| x = y})
16		anr	a = the A /\ A == {x \| x = y} -> A == {x \| x = y}
17	15, 16	mpbird	a = the A /\ A == {x \| x = y} -> A == {x \| x = a}
18	17	orld	a = the A /\ A == {x \| x = y} -> A == {x \| x = a} \/ ~E. y A == {x \| x = y} /\ a = 0
19	18	exp	a = the A -> A == {x \| x = y} -> A == {x \| x = a} \/ ~E. y A == {x \| x = y} /\ a = 0
20	1, 7, 19	eexdh	a = the A -> E. y A == {x \| x = y} -> A == {x \| x = a} \/ ~E. y A == {x \| x = y} /\ a = 0
21	20	imp	a = the A /\ E. y A == {x \| x = y} -> A == {x \| x = a} \/ ~E. y A == {x \| x = y} /\ a = 0
22		anr	a = the A /\ ~E. y A == {x \| x = y} -> ~E. y A == {x \| x = y}
23		anl	a = the A /\ ~E. y A == {x \| x = y} -> a = the A
24		the0	~E. y A == {x \| x = y} -> the A = 0
25	24	anwr	a = the A /\ ~E. y A == {x \| x = y} -> the A = 0
26	23, 25	eqtrd	a = the A /\ ~E. y A == {x \| x = y} -> a = 0
27	22, 26	iand	a = the A /\ ~E. y A == {x \| x = y} -> ~E. y A == {x \| x = y} /\ a = 0
28	27	orrd	a = the A /\ ~E. y A == {x \| x = y} -> A == {x \| x = a} \/ ~E. y A == {x \| x = y} /\ a = 0
29	21, 28	casesda	a = the A -> A == {x \| x = a} \/ ~E. y A == {x \| x = y} /\ a = 0
30		eor	(A == {x \| x = a} -> a = the A) -> (~E. y A == {x \| x = y} /\ a = 0 -> a = the A) -> A == {x \| x = a} \/ ~E. y A == {x \| x = y} /\ a = 0 -> a = the A
31		theid	A == {x \| x = a} -> the A = a
32	31	eqcomd	A == {x \| x = a} -> a = the A
33	30, 32	ax_mp	(~E. y A == {x \| x = y} /\ a = 0 -> a = the A) -> A == {x \| x = a} \/ ~E. y A == {x \| x = y} /\ a = 0 -> a = the A
34		anr	~E. y A == {x \| x = y} /\ a = 0 -> a = 0
35	24	eqcomd	~E. y A == {x \| x = y} -> 0 = the A
36	35	anwl	~E. y A == {x \| x = y} /\ a = 0 -> 0 = the A
37	34, 36	eqtrd	~E. y A == {x \| x = y} /\ a = 0 -> a = the A
38	33, 37	ax_mp	A == {x \| x = a} \/ ~E. y A == {x \| x = y} /\ a = 0 -> a = the A
39	29, 38	ibii	a = the A <-> A == {x \| x = a} \/ ~E. y A == {x \| x = y} /\ 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)