axacnd - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > axacnd		Structured version Visualization version Unicode version

Theorem axacnd 9434

Description: A version of the Axiom of Choice with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 3-Jan-2002.) (Proof shortened by Mario Carneiro, 10-Dec-2016.)

**Assertion**
Ref	Expression
axacnd	$/\$ $/\$ $/\$ $/\$

Proof of Theorem axacnd Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		axacndlem5 9433	. . . 4 $/\$ $/\$ $/\$ $/\$
2		nfnae 2318	. . . . . 6
3		nfnae 2318	. . . . . 6
4		nfnae 2318	. . . . . 6
5	2, 3, 4	nf3an 1831	. . . . 5 $/\$ $/\$
6		nfnae 2318	. . . . . . 7
7		nfnae 2318	. . . . . . 7
8		nfnae 2318	. . . . . . 7
9	6, 7, 8	nf3an 1831	. . . . . 6 $/\$ $/\$
10		nfnae 2318	. . . . . . . 8
11		nfnae 2318	. . . . . . . 8
12		nfnae 2318	. . . . . . . 8
13	10, 11, 12	nf3an 1831	. . . . . . 7 $/\$ $/\$
14		nfcvf 2788	. . . . . . . . . . . 12
15	14	3ad2ant2 1083	. . . . . . . . . . 11 $/\$ $/\$
16		nfcvd 2765	. . . . . . . . . . 11 $/\$ $/\$
17	15, 16	nfeld 2773	. . . . . . . . . 10 $/\$ $/\$
18		nfcvf 2788	. . . . . . . . . . . 12
19	18	3ad2ant3 1084	. . . . . . . . . . 11 $/\$ $/\$
20	16, 19	nfeld 2773	. . . . . . . . . 10 $/\$ $/\$
21	17, 20	nfand 1826	. . . . . . . . 9 $/\$ $/\$ $/\$
22	5, 21	nfald 2165	. . . . . . . 8 $/\$ $/\$ $/\$
23		nfnae 2318	. . . . . . . . . 10
24		nfnae 2318	. . . . . . . . . 10
25		nfnae 2318	. . . . . . . . . 10
26	23, 24, 25	nf3an 1831	. . . . . . . . 9 $/\$ $/\$
27	15, 19	nfeld 2773	. . . . . . . . . . . . . 14 $/\$ $/\$
28		nfcvf 2788	. . . . . . . . . . . . . . . 16
29	28	3ad2ant1 1082	. . . . . . . . . . . . . . 15 $/\$ $/\$
30	19, 29	nfeld 2773	. . . . . . . . . . . . . 14 $/\$ $/\$
31	27, 30	nfand 1826	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
32	21, 31	nfand 1826	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
33	26, 32	nfexd 2167	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
34	15, 19	nfeqd 2772	. . . . . . . . . . 11 $/\$ $/\$
35	33, 34	nfbid 1832	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
36	9, 35	nfald 2165	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
37	26, 36	nfexd 2167	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
38	22, 37	nfimd 1823	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39		nfcvd 2765	. . . . . . . . . . . 12 $/\$ $/\$
40		nfcvf2 2789	. . . . . . . . . . . . 13
41	40	3ad2ant1 1082	. . . . . . . . . . . 12 $/\$ $/\$
42	39, 41	nfeqd 2772	. . . . . . . . . . 11 $/\$ $/\$
43	5, 42	nfan1 2068	. . . . . . . . . 10 $/\$ $/\$ $/\$
44		simpr 477	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
45	44	eleq2d 2687	. . . . . . . . . . 11 $/\$ $/\$ $/\$
46	44	eleq1d 2686	. . . . . . . . . . 11 $/\$ $/\$ $/\$
47	45, 46	anbi12d 747	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
48	43, 47	albid 2090	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
49		nfcvd 2765	. . . . . . . . . . . 12 $/\$ $/\$
50		nfcvf2 2789	. . . . . . . . . . . . 13
51	50	3ad2ant3 1084	. . . . . . . . . . . 12 $/\$ $/\$
52	49, 51	nfeqd 2772	. . . . . . . . . . 11 $/\$ $/\$
53	26, 52	nfan1 2068	. . . . . . . . . 10 $/\$ $/\$ $/\$
54		nfcvd 2765	. . . . . . . . . . . . 13 $/\$ $/\$
55		nfcvf2 2789	. . . . . . . . . . . . . 14
56	55	3ad2ant2 1083	. . . . . . . . . . . . 13 $/\$ $/\$
57	54, 56	nfeqd 2772	. . . . . . . . . . . 12 $/\$ $/\$
58	9, 57	nfan1 2068	. . . . . . . . . . 11 $/\$ $/\$ $/\$
59	47	anbi1d 741	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60	53, 59	exbid 2091	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	60	bibi1d 333	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62	58, 61	albid 2090	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63	53, 62	exbid 2091	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64	48, 63	imbi12d 334	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65	64	ex 450	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66	13, 38, 65	cbvald 2277	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67	9, 66	albid 2090	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68	5, 67	exbid 2091	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69	1, 68	mpbii 223	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70	69	3exp 1264	. 2 $/\$ $/\$ $/\$ $/\$
71		axacndlem2 9430	. . 3 $/\$ $/\$ $/\$ $/\$
72	71	aecoms 2312	. 2 $/\$ $/\$ $/\$ $/\$
73		axacndlem3 9431	. . 3 $/\$ $/\$ $/\$ $/\$
74	73	aecoms 2312	. 2 $/\$ $/\$ $/\$ $/\$
75		nfae 2316	. . . 4
76		simpr 477	. . . . . . 7 $/\$
77	76	alimi 1739	. . . . . 6 $/\$
78		nd3 9411	. . . . . . 7
79	78	pm2.21d 118	. . . . . 6 $/\$ $/\$ $/\$
80	77, 79	syl5 34	. . . . 5 $/\$ $/\$ $/\$ $/\$
81	80	axc4i 2131	. . . 4 $/\$ $/\$ $/\$ $/\$
82	75, 81	alrimi 2082	. . 3 $/\$ $/\$ $/\$ $/\$
83		19.8a 2052	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
84	82, 83	syl 17	. 2 $/\$ $/\$ $/\$ $/\$
85	70, 72, 74, 84	pm2.61iii 179	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $/\$ wa 384 $/\$ w3a 1037

wal 1481

wex 1704

wnfc 2751

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906 ax-reg 8497 ax-ac 9281

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-br 4654 df-opab 4713 df-eprel 5029 df-fr 5073

This theorem is referenced by: zfcndac 9441 axacprim 31584

W3C validator