ac6s6 - Mathbox for Giovanni Mascellani

	Mathbox for Giovanni Mascellani		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ac6s6		Structured version Visualization version Unicode version

Theorem ac6s6 33980

Description: Generalization of the Axiom of Choice to classes, moving the existence condition in the consequent. (Contributed by Giovanni Mascellani, 19-Aug-2018.)

**Hypotheses**
Ref	Expression
ac6s6.1
ac6s6.2
ac6s6.3

**Assertion**
Ref	Expression
ac6s6

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

**Proof of Theorem ac6s6**
Step	Hyp	Ref	Expression
1		hbe1 2021	. . . . . 6
2		iftrue 4092	. . . . . . 7
3	2	abeq2d 2734	. . . . . 6
4	1, 3	exbidh 1794	. . . . 5
5	4	ibir 257	. . . 4
6		vex 3203	. . . . . 6
7	6	exiftru 1891	. . . . 5
8	1	hbn 2146	. . . . . 6
9		iffalse 4095	. . . . . . 7
10	9	eleq2d 2687	. . . . . 6
11	8, 10	exbidh 1794	. . . . 5
12	7, 11	mpbiri 248	. . . 4
13	5, 12	pm2.61i 176	. . 3
14	13	rgenw 2924	. 2
15		nfe1 2027	. . . 4
16		ac6s6.1	. . . 4
17	15, 16	nfim 1825	. . 3
18		ac6s6.2	. . 3
19		ac6s6.3	. . . . . 6
20		id 22	. . . . . . . . . . . . . . 15
21	20	a1i 11	. . . . . . . . . . . . . 14
22		ax-1 6	. . . . . . . . . . . . . . . . . . 19
23		tsim3 33939	. . . . . . . . . . . . . . . . . . . 20 $\/$
24	23	a1d 25	. . . . . . . . . . . . . . . . . . 19 $\/$
25	22, 24	cnf2dd 33893	. . . . . . . . . . . . . . . . . 18
26		tsim3 33939	. . . . . . . . . . . . . . . . . . 19 $\/$
27	26	a1d 25	. . . . . . . . . . . . . . . . . 18 $\/$
28	25, 27	cnf2dd 33893	. . . . . . . . . . . . . . . . 17
29		tsim2 33938	. . . . . . . . . . . . . . . . . 18 $\/$
30	29	a1d 25	. . . . . . . . . . . . . . . . 17 $\/$
31	28, 30	cnf2dd 33893	. . . . . . . . . . . . . . . 16
32		tsim2 33938	. . . . . . . . . . . . . . . . . 18 $\/$
33	32	a1d 25	. . . . . . . . . . . . . . . . 17 $\/$
34	25, 33	cnf2dd 33893	. . . . . . . . . . . . . . . 16
35	31, 34	mpdd 43	. . . . . . . . . . . . . . 15
36		tsbi4 33943	. . . . . . . . . . . . . . . 16 $\/$ $\/$
37	36	a1d 25	. . . . . . . . . . . . . . 15 $\/$ $\/$
38	35, 37	cnfn2dd 33895	. . . . . . . . . . . . . 14 $\/$
39	21, 38	cnf2dd 33893	. . . . . . . . . . . . 13
40		tsim3 33939	. . . . . . . . . . . . . . . . 17 $\/$
41	40	a1d 25	. . . . . . . . . . . . . . . 16 $\/$
42	28, 41	cnf2dd 33893	. . . . . . . . . . . . . . 15
43		tsim3 33939	. . . . . . . . . . . . . . . 16 $\/$
44	43	a1d 25	. . . . . . . . . . . . . . 15 $\/$
45	42, 44	cnf2dd 33893	. . . . . . . . . . . . . 14
46		tsbi2 33941	. . . . . . . . . . . . . . 15 $\/$ $\/$
47	46	a1d 25	. . . . . . . . . . . . . 14 $\/$ $\/$
48	45, 47	cnf2dd 33893	. . . . . . . . . . . . 13 $\/$
49	39, 48	cnf1dd 33892	. . . . . . . . . . . 12
50		tsim2 33938	. . . . . . . . . . . . . . . . . . 19 $\/$
51	50	a1d 25	. . . . . . . . . . . . . . . . . 18 $\/$
52	42, 51	cnf2dd 33893	. . . . . . . . . . . . . . . . 17
53		simplim 163	. . . . . . . . . . . . . . . . 17
54	52, 53	syld 47	. . . . . . . . . . . . . . . 16
55		tsbi3 33942	. . . . . . . . . . . . . . . . 17 $\/$ $\/$
56	55	a1d 25	. . . . . . . . . . . . . . . 16 $\/$ $\/$
57	54, 56	cnfn2dd 33895	. . . . . . . . . . . . . . 15 $\/$
58	21, 57	cnf1dd 33892	. . . . . . . . . . . . . 14
59		tsim1 33937	. . . . . . . . . . . . . . . 16 $\/$ $\/$
60	59	a1d 25	. . . . . . . . . . . . . . 15 $\/$ $\/$
61	60	or32dd 33896	. . . . . . . . . . . . . 14 $\/$ $\/$
62	58, 61	cnf2dd 33893	. . . . . . . . . . . . 13 $\/$
63	31, 62	cnfn1dd 33894	. . . . . . . . . . . 12
64	49, 63	contrd 33899	. . . . . . . . . . 11
65	64	a1d 25	. . . . . . . . . 10
66		ax-1 6	. . . . . . . . . . . . . . 15
67	23	a1d 25	. . . . . . . . . . . . . . 15 $\/$
68	66, 67	cnf2dd 33893	. . . . . . . . . . . . . 14
69	26	a1d 25	. . . . . . . . . . . . . 14 $\/$
70	68, 69	cnf2dd 33893	. . . . . . . . . . . . 13
71	29	a1d 25	. . . . . . . . . . . . 13 $\/$
72	70, 71	cnf2dd 33893	. . . . . . . . . . . 12
73	32	a1d 25	. . . . . . . . . . . . 13 $\/$
74	68, 73	cnf2dd 33893	. . . . . . . . . . . 12
75	72, 74	mpdd 43	. . . . . . . . . . 11
76		tsbi3 33942	. . . . . . . . . . . 12 $\/$ $\/$
77	76	a1d 25	. . . . . . . . . . 11 $\/$ $\/$
78	75, 77	cnfn2dd 33895	. . . . . . . . . 10 $\/$
79	65, 78	cnfn2dd 33895	. . . . . . . . 9
80	40	a1d 25	. . . . . . . . . . . . . . . 16 $\/$
81	70, 80	cnf2dd 33893	. . . . . . . . . . . . . . 15
82	50	a1d 25	. . . . . . . . . . . . . . 15 $\/$
83	81, 82	cnf2dd 33893	. . . . . . . . . . . . . 14
84	83, 53	syld 47	. . . . . . . . . . . . 13
85		tsbi4 33943	. . . . . . . . . . . . . 14 $\/$ $\/$
86	85	a1d 25	. . . . . . . . . . . . 13 $\/$ $\/$
87	84, 86	cnfn2dd 33895	. . . . . . . . . . . 12 $\/$
88	65, 87	cnfn1dd 33894	. . . . . . . . . . 11
89	88	a1dd 50	. . . . . . . . . 10
90		tsbi1 33940	. . . . . . . . . . . 12 $\/$ $\/$
91	90	a1d 25	. . . . . . . . . . 11 $\/$ $\/$
92	91	or32dd 33896	. . . . . . . . . 10 $\/$ $\/$
93	89, 92	cnfn2dd 33895	. . . . . . . . 9 $\/$
94	79, 93	cnfn1dd 33894	. . . . . . . 8
95	43	a1d 25	. . . . . . . . 9 $\/$
96	81, 95	cnf2dd 33893	. . . . . . . 8
97	94, 96	contrd 33899	. . . . . . 7
98	97	efald2 33877	. . . . . 6
99	19, 98	ax-mp 5	. . . . 5
100	3, 99	ax-mp 5	. . . 4
101	6	a1i 11	. . . . . . 7
102		id 22	. . . . . . . . . . . 12
103		tsim2 33938	. . . . . . . . . . . . . . 15 $\/$
104	103	ord 392	. . . . . . . . . . . . . 14
105	104	a1dd 50	. . . . . . . . . . . . 13
106	105	a1dd 50	. . . . . . . . . . . 12
107	102, 106	mt3d 140	. . . . . . . . . . 11
108	107	a1d 25	. . . . . . . . . 10
109		simplim 163	. . . . . . . . . 10
110	108, 109	syld 47	. . . . . . . . 9
111		tsim2 33938	. . . . . . . . . . . . . 14 $\/$
112	111	ord 392	. . . . . . . . . . . . 13
113	112	a1dd 50	. . . . . . . . . . . 12
114	102, 113	mt3d 140	. . . . . . . . . . 11
115	108, 114	syld 47	. . . . . . . . . 10
116		id 22	. . . . . . . . . . . . . . . . . 18 $\/$ $\/$
117	116	notornotel2 33898	. . . . . . . . . . . . . . . . 17 $\/$
118	117	a1i 11	. . . . . . . . . . . . . . . 16 $\/$
119	116	notornotel1 33897	. . . . . . . . . . . . . . . . . 18 $\/$
120	119	a1i 11	. . . . . . . . . . . . . . . . 17 $\/$
121		tsbi3 33942	. . . . . . . . . . . . . . . . . 18 $\/$ $\/$
122	121	a1d 25	. . . . . . . . . . . . . . . . 17 $\/$ $\/$ $\/$
123	120, 122	cnfn2dd 33895	. . . . . . . . . . . . . . . 16 $\/$ $\/$
124	118, 123	cnfn2dd 33895	. . . . . . . . . . . . . . 15 $\/$
125		a1tru 1500	. . . . . . . . . . . . . . . . 17
126	125	a1d 25	. . . . . . . . . . . . . . . 16 $\/$
127		tsbi1 33940	. . . . . . . . . . . . . . . . . 18 $\/$ $\/$
128	127	a1d 25	. . . . . . . . . . . . . . . . 17 $\/$ $\/$ $\/$
129	128	or32dd 33896	. . . . . . . . . . . . . . . 16 $\/$ $\/$ $\/$
130	126, 129	cnfn2dd 33895	. . . . . . . . . . . . . . 15 $\/$ $\/$
131	124, 130	cnfn1dd 33894	. . . . . . . . . . . . . 14 $\/$
132	131	a1dd 50	. . . . . . . . . . . . 13 $\/$
133	132	a1dd 50	. . . . . . . . . . . 12 $\/$
134		ax-1 6	. . . . . . . . . . . . 13 $\/$
135		tsim3 33939	. . . . . . . . . . . . . 14 $\/$
136	135	a1d 25	. . . . . . . . . . . . 13 $\/$ $\/$
137	134, 136	cnf2dd 33893	. . . . . . . . . . . 12 $\/$
138	133, 137	contrd 33899	. . . . . . . . . . 11 $\/$
139	138	a1d 25	. . . . . . . . . 10 $\/$
140	115, 139	cnfn1dd 33894	. . . . . . . . 9
141	110, 140	contrd 33899	. . . . . . . 8
142	141	efald2 33877	. . . . . . 7
143	101, 142	ax-mp 5	. . . . . 6
144	10, 143	ax-mp 5	. . . . 5
145		ax-1 6	. . . . . . . . . 10
146		tsim3 33939	. . . . . . . . . . 11 $\/$
147	146	a1d 25	. . . . . . . . . 10 $\/$
148	145, 147	cnf2dd 33893	. . . . . . . . 9
149		tsim2 33938	. . . . . . . . . 10 $\/$
150	149	a1d 25	. . . . . . . . 9 $\/$
151	148, 150	cnf2dd 33893	. . . . . . . 8
152		tsim2 33938	. . . . . . . . . 10 $\/$
153	152	a1d 25	. . . . . . . . 9 $\/$
154	145, 153	cnf2dd 33893	. . . . . . . 8
155	151, 154	mpdd 43	. . . . . . 7
156		id 22	. . . . . . . . . . 11
157		id 22	. . . . . . . . . . . . . . 15
158	157	a1i 11	. . . . . . . . . . . . . 14
159		tsim2 33938	. . . . . . . . . . . . . . 15 $\/$
160	159	a1d 25	. . . . . . . . . . . . . 14 $\/$
161	158, 160	cnf2dd 33893	. . . . . . . . . . . . 13
162	149	a1d 25	. . . . . . . . . . . . 13 $\/$
163	161, 162	cnfn1dd 33894	. . . . . . . . . . . 12
164	163	a1dd 50	. . . . . . . . . . 11
165	156, 164	mt3d 140	. . . . . . . . . 10
166	165	a1d 25	. . . . . . . . 9
167		tsim3 33939	. . . . . . . . . . . . 13 $\/$
168	167	a1d 25	. . . . . . . . . . . 12 $\/$
169	148, 168	cnf2dd 33893	. . . . . . . . . . 11
170		tsim3 33939	. . . . . . . . . . . 12 $\/$
171	170	a1d 25	. . . . . . . . . . 11 $\/$
172	169, 171	cnf2dd 33893	. . . . . . . . . 10
173		tsbi1 33940	. . . . . . . . . . 11 $\/$ $\/$
174	173	a1d 25	. . . . . . . . . 10 $\/$ $\/$
175	172, 174	cnf2dd 33893	. . . . . . . . 9 $\/$
176	166, 175	cnfn2dd 33895	. . . . . . . 8
177		a1tru 1500	. . . . . . . . . 10
178	177	a1d 25	. . . . . . . . 9
179		tsbi3 33942	. . . . . . . . . . 11 $\/$ $\/$
180	179	a1d 25	. . . . . . . . . 10 $\/$ $\/$
181	180	or32dd 33896	. . . . . . . . 9 $\/$ $\/$
182	178, 181	cnfn2dd 33895	. . . . . . . 8 $\/$
183	176, 182	cnf1dd 33892	. . . . . . 7
184	155, 183	contrd 33899	. . . . . 6
185	184	efald2 33877	. . . . 5
186	144, 185	ax-mp 5	. . . 4
187	100, 186	pm2.61i 176	. . 3
188	17, 18, 187	ac6s3f 33979	. 2
189	14, 188	ax-mp 5	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383

wceq 1483

wtru 1484

wfal 1488

wex 1704

wnf 1708

wcel 1990

cab 2608

wral 2912

cvv 3200

cif 4086

cfv 5888

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-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-reg 8497 ax-inf2 8538 ax-ac2 9285

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 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-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-om 7066 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-en 7956 df-r1 8627 df-rank 8628 df-card 8765 df-ac 8939

This theorem is referenced by: ac6s6f 33981

W3C validator