![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > kmlem9 | Unicode version |
Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004.) |
Ref | Expression |
---|---|
kmlem9.1 |
Ref | Expression |
---|---|
kmlem9 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3112 | . . . 4 | |
2 | eqeq1 2461 | . . . . 5 | |
3 | 2 | rexbidv 2968 | . . . 4 |
4 | kmlem9.1 | . . . 4 | |
5 | 1, 3, 4 | elab2 3249 | . . 3 |
6 | vex 3112 | . . . . 5 | |
7 | eqeq1 2461 | . . . . . 6 | |
8 | 7 | rexbidv 2968 | . . . . 5 |
9 | 6, 8, 4 | elab2 3249 | . . . 4 |
10 | difeq1 3614 | . . . . . . 7 | |
11 | sneq 4039 | . . . . . . . . . 10 | |
12 | 11 | difeq2d 3621 | . . . . . . . . 9 |
13 | 12 | unieqd 4259 | . . . . . . . 8 |
14 | 13 | difeq2d 3621 | . . . . . . 7 |
15 | 10, 14 | eqtrd 2498 | . . . . . 6 |
16 | 15 | eqeq2d 2471 | . . . . 5 |
17 | 16 | cbvrexv 3085 | . . . 4 |
18 | 9, 17 | bitri 249 | . . 3 |
19 | reeanv 3025 | . . . 4 | |
20 | eqeq12 2476 | . . . . . . . . . 10 | |
21 | 15, 20 | syl5ibr 221 | . . . . . . . . 9 |
22 | 21 | necon3d 2681 | . . . . . . . 8 |
23 | kmlem5 8555 | . . . . . . . . . 10 | |
24 | ineq12 3694 | . . . . . . . . . . 11 | |
25 | 24 | eqeq1d 2459 | . . . . . . . . . 10 |
26 | 23, 25 | syl5ibr 221 | . . . . . . . . 9 |
27 | 26 | expd 436 | . . . . . . . 8 |
28 | 22, 27 | syl5d 67 | . . . . . . 7 |
29 | 28 | com12 31 | . . . . . 6 |
30 | 29 | adantl 466 | . . . . 5 |
31 | 30 | rexlimivv 2954 | . . . 4 |
32 | 19, 31 | sylbir 213 | . . 3 |
33 | 5, 18, 32 | syl2anb 479 | . 2 |
34 | 33 | rgen2a 2884 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -> wi 4 /\ wa 369
= wceq 1395 e. wcel 1818 { cab 2442
=/= wne 2652 A. wral 2807 E. wrex 2808
\ cdif 3472 i^i cin 3474 c0 3784 { csn 4029 U. cuni 4249 |
This theorem is referenced by: kmlem10 8560 |
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-in 3482 df-ss 3489 df-nul 3785 df-sn 4030 df-uni 4250 |
Copyright terms: Public domain | W3C validator |