Theorem kmlem3 8553

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. The right-hand side is part of the hypothesis of 4. (Contributed by NM, 25-Mar-2004.)

Assertion

Ref	Expression
kmlem3

Distinct variable group:   ,,,

Proof of Theorem kmlem3

Step	Hyp	Ref	Expression
1		dfdif2 3484	. . . 4
2		dfnul3 3787	. . . . . 6
3	2	uneq2i 3654	. . . . 5
4		un0 3810	. . . . 5
5		unrab 3768	. . . . 5
6	3, 4, 5	3eqtr3i 2494	. . . 4
7		ianor 488	. . . . . . 7
8		eluni 4252	. . . . . . . . . 10
9	8	anbi1i 695	. . . . . . . . 9
10		df-rex 2813	. . . . . . . . . 10
11		elin 3686	. . . . . . . . . . . . . . 15
12	11	anbi2i 694	. . . . . . . . . . . . . 14
13		df-an 371	. . . . . . . . . . . . . 14
14	12, 13	bitr3i 251	. . . . . . . . . . . . 13
15	14	anbi2i 694	. . . . . . . . . . . 12
16		eldifsn 4155	. . . . . . . . . . . . . . . 16
17		necom 2726	. . . . . . . . . . . . . . . . 17
18	17	anbi2i 694	. . . . . . . . . . . . . . . 16
19	16, 18	bitri 249	. . . . . . . . . . . . . . 15
20	19	anbi2i 694	. . . . . . . . . . . . . 14
21		ancom 450	. . . . . . . . . . . . . . 15
22	21	anbi2ci 696	. . . . . . . . . . . . . 14
23		anass 649	. . . . . . . . . . . . . 14
24	20, 22, 23	3bitri 271	. . . . . . . . . . . . 13
25		an32 798	. . . . . . . . . . . . 13
26	24, 25	bitr3i 251	. . . . . . . . . . . 12
27	15, 26	bitr3i 251	. . . . . . . . . . 11
28	27	exbii 1667	. . . . . . . . . 10
29		19.41v 1771	. . . . . . . . . 10
30	10, 28, 29	3bitri 271	. . . . . . . . 9
31		rexnal 2905	. . . . . . . . 9
32	9, 30, 31	3bitr2ri 274	. . . . . . . 8
33	32	con1bii 331	. . . . . . 7
34	7, 33	bitr3i 251	. . . . . 6
35	34	a1i 11	. . . . 5
36	35	rabbiia 3098	. . . 4
37	1, 6, 36	3eqtri 2490	. . 3
38	37	neeq1i 2742	. 2
39		rabn0 3805	. 2
40	38, 39	bitri 249	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  /\wa 369  E.wex 1612  e.wcel 1818  =/=wne 2652  A.wral 2807  E.wrex 2808  {crab 2811  \cdif 3472  u.cun 3473  i^icin 3474  c0 3784  {csn 4029  U.cuni 4249

This theorem is referenced by:  kmlem13  8563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-nul 3785  df-sn 4030  df-uni 4250