ac - Higher-Order Logic Explorer

	Higher-Order Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > HOLE Home > Th. List > ac		Unicode version

Theorem ac 184

Description: Defining property of the indefinite descriptor: it selects an element from any type. This is equivalent to global choice in ZF.

**Hypotheses**
Ref	Expression
ac.1
ac.2

**Assertion**
Ref	Expression
ac

Proof of Theorem ac Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ac.1	. . 3
2		wat 180	. . . 4
3	2, 1	wc 45	. . 3
4	1, 3	wc 45	. 2
5		ac.2	. . . 4
6	1, 5	wc 45	. . 3
7	6	id 25	. 2
8	7	ax-cb1 29	. . 3
9		ax-ac 183	. . . . 5
10		wal 124	. . . . . . 7
11		wim 127	. . . . . . . . 9
12		wv 58	. . . . . . . . . 10
13		wv 58	. . . . . . . . . 10
14	12, 13	wc 45	. . . . . . . . 9
15	2, 12	wc 45	. . . . . . . . . 10
16	12, 15	wc 45	. . . . . . . . 9
17	11, 14, 16	wov 64	. . . . . . . 8
18	17	wl 59	. . . . . . 7
19	10, 18	wc 45	. . . . . 6
20	12, 1	weqi 68	. . . . . . . . . . 11
21	20	id 25	. . . . . . . . . 10
22	12, 13, 21	ceq1 79	. . . . . . . . 9
23	2, 12, 21	ceq2 80	. . . . . . . . . 10
24	12, 15, 21, 23	ceq12 78	. . . . . . . . 9
25	11, 14, 16, 22, 24	oveq12 90	. . . . . . . 8
26	17, 25	leq 81	. . . . . . 7
27	10, 18, 26	ceq2 80	. . . . . 6
28	19, 1, 27	cla4v 142	. . . . 5
29	9, 28	syl 16	. . . 4
30	17, 25	eqtypi 69	. . . . 5
31	1, 13	wc 45	. . . . . 6
32	13, 5	weqi 68	. . . . . . . 8
33	32	id 25	. . . . . . 7
34	1, 13, 33	ceq2 80	. . . . . 6
35	11, 31, 4, 34	oveq1 89	. . . . 5
36	30, 5, 35	cla4v 142	. . . 4
37	29, 36	syl 16	. . 3
38	8, 37	a1i 28	. 2
39	4, 7, 38	mpd 146	1