axacndlem4 - Metamath Proof Explorer

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

Theorem axacndlem4 9432

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

**Assertion**
Ref	Expression
axacndlem4	$/\$ $/\$ $/\$ $/\$

Distinct variable group:

Proof of Theorem axacndlem4 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		zfac 9282	. . . 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	. . . . . . . . . . 11
15	14	3ad2ant2 1083	. . . . . . . . . 10 $/\$ $/\$
16		nfcvf 2788	. . . . . . . . . . 11
17	16	3ad2ant1 1082	. . . . . . . . . 10 $/\$ $/\$
18	15, 17	nfeld 2773	. . . . . . . . 9 $/\$ $/\$
19		nfcvf 2788	. . . . . . . . . . 11
20	19	3ad2ant3 1084	. . . . . . . . . 10 $/\$ $/\$
21	17, 20	nfeld 2773	. . . . . . . . 9 $/\$ $/\$
22	18, 21	nfand 1826	. . . . . . . 8 $/\$ $/\$ $/\$
23		nfnae 2318	. . . . . . . . . 10
24		nfnae 2318	. . . . . . . . . 10
25		nfnae 2318	. . . . . . . . . 10
26	23, 24, 25	nf3an 1831	. . . . . . . . 9 $/\$ $/\$
27	15, 20	nfeld 2773	. . . . . . . . . . . . . 14 $/\$ $/\$
28		nfcvd 2765	. . . . . . . . . . . . . . 15 $/\$ $/\$
29	20, 28	nfeld 2773	. . . . . . . . . . . . . 14 $/\$ $/\$
30	27, 29	nfand 1826	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
31	22, 30	nfand 1826	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
32	26, 31	nfexd 2167	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
33	15, 20	nfeqd 2772	. . . . . . . . . . 11 $/\$ $/\$
34	32, 33	nfbid 1832	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
35	9, 34	nfald 2165	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
36	26, 35	nfexd 2167	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
37	22, 36	nfimd 1823	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38	13, 37	nfald 2165	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39	9, 38	nfald 2165	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		nfcvd 2765	. . . . . . . . 9 $/\$ $/\$
41		nfcvf2 2789	. . . . . . . . . 10
42	41	3ad2ant2 1083	. . . . . . . . 9 $/\$ $/\$
43	40, 42	nfeqd 2772	. . . . . . . 8 $/\$ $/\$
44	9, 43	nfan1 2068	. . . . . . 7 $/\$ $/\$ $/\$
45		nfcvd 2765	. . . . . . . . . 10 $/\$ $/\$
46		nfcvf2 2789	. . . . . . . . . . 11
47	46	3ad2ant1 1082	. . . . . . . . . 10 $/\$ $/\$
48	45, 47	nfeqd 2772	. . . . . . . . 9 $/\$ $/\$
49	13, 48	nfan1 2068	. . . . . . . 8 $/\$ $/\$ $/\$
50	22	nf5rd 2066	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
51	50	adantr 481	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
52		sp 2053	. . . . . . . . . 10 $/\$ $/\$
53	51, 52	impbid1 215	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
54		nfcvd 2765	. . . . . . . . . . . 12 $/\$ $/\$
55		nfcvf2 2789	. . . . . . . . . . . . 13
56	55	3ad2ant3 1084	. . . . . . . . . . . 12 $/\$ $/\$
57	54, 56	nfeqd 2772	. . . . . . . . . . 11 $/\$ $/\$
58	26, 57	nfan1 2068	. . . . . . . . . 10 $/\$ $/\$ $/\$
59		simpr 477	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
60	59	eleq2d 2687	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
61	60	anbi2d 740	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
62	61	anbi2d 740	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63	58, 62	exbid 2091	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64	63	bibi1d 333	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65	44, 64	albid 2090	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66	58, 65	exbid 2091	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67	53, 66	imbi12d 334	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68	49, 67	albid 2090	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69	44, 68	albid 2090	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70	69	ex 450	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71	5, 39, 70	cbvexd 2278	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72	1, 71	mpbii 223	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
73	72	3exp 1264	. 2 $/\$ $/\$ $/\$ $/\$
74		axacndlem2 9430	. 2 $/\$ $/\$ $/\$ $/\$
75		axacndlem1 9429	. 2 $/\$ $/\$ $/\$ $/\$
76		nfae 2316	. . . 4
77		nfae 2316	. . . . 5
78		simpr 477	. . . . . . 7 $/\$
79	78	alimi 1739	. . . . . 6 $/\$
80		nd2 9410	. . . . . . 7
81	80	pm2.21d 118	. . . . . 6 $/\$ $/\$ $/\$
82	79, 81	syl5 34	. . . . 5 $/\$ $/\$ $/\$ $/\$
83	77, 82	alrimi 2082	. . . 4 $/\$ $/\$ $/\$ $/\$
84	76, 83	alrimi 2082	. . 3 $/\$ $/\$ $/\$ $/\$
85		19.8a 2052	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86	84, 85	syl 17	. 2 $/\$ $/\$ $/\$ $/\$
87	73, 74, 75, 86	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-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-v 3202 df-dif 3577 df-un 3579 df-nul 3916 df-sn 4178 df-pr 4180

This theorem is referenced by: axacndlem5 9433

W3C validator