Description: A basis is not affected by the addition or removal of the empty set. (Contributed by Mario Carneiro, 28-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | basdif0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssun1 | |
|
2 | undif1 | |
|
3 | 1 2 | sseqtrri | |
4 | snex | |
|
5 | unexg | |
|
6 | 4 5 | mpan2 | |
7 | ssexg | |
|
8 | 3 6 7 | sylancr | |
9 | elex | |
|
10 | indif1 | |
|
11 | 10 | unieqi | |
12 | unidif0 | |
|
13 | 11 12 | eqtri | |
14 | 13 | sseq2i | |
15 | 14 | ralbii | |
16 | inss2 | |
|
17 | elinel2 | |
|
18 | elsni | |
|
19 | 17 18 | syl | |
20 | 0ss | |
|
21 | 19 20 | eqsstrdi | |
22 | 16 21 | sstrid | |
23 | 22 | rgen | |
24 | ralunb | |
|
25 | 23 24 | mpbiran | |
26 | inundif | |
|
27 | 26 | raleqi | |
28 | 15 25 27 | 3bitr2i | |
29 | 28 | ralbii | |
30 | inss1 | |
|
31 | elinel2 | |
|
32 | elsni | |
|
33 | 31 32 | syl | |
34 | 33 20 | eqsstrdi | |
35 | 30 34 | sstrid | |
36 | 35 | ralrimivw | |
37 | 36 | rgen | |
38 | ralunb | |
|
39 | 37 38 | mpbiran | |
40 | 26 | raleqi | |
41 | 29 39 40 | 3bitr2i | |
42 | 41 | a1i | |
43 | difexg | |
|
44 | isbasisg | |
|
45 | 43 44 | syl | |
46 | isbasisg | |
|
47 | 42 45 46 | 3bitr4d | |
48 | 8 9 47 | pm5.21nii | |