basdif0 - Metamath Proof Explorer

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

Theorem basdif0 20757

Description: A basis is not affected by the addition or removal of the empty set. (Contributed by Mario Carneiro, 28-Aug-2015.)

**Assertion**
Ref	Expression
basdif0	$\$

Proof of Theorem basdif0 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssun1 3776	. . . 4
2		undif1 4043	. . . 4 $\$
3	1, 2	sseqtr4i 3638	. . 3 $\$
4		snex 4908	. . . 4
5		unexg 6959	. . . 4 $\$ $/\$ $\$
6	4, 5	mpan2 707	. . 3 $\$ $\$
7		ssexg 4804	. . 3 $\$ $/\$ $\$
8	3, 6, 7	sylancr 695	. 2 $\$
9		elex 3212	. 2
10		indif1 3871	. . . . . . . . . . 11 $\$ $\$
11	10	unieqi 4445	. . . . . . . . . 10 $\$ $\$
12		unidif0 4838	. . . . . . . . . 10 $\$
13	11, 12	eqtri 2644	. . . . . . . . 9 $\$
14	13	sseq2i 3630	. . . . . . . 8 $\$
15	14	ralbii 2980	. . . . . . 7 $\$ $\$ $\$
16		inss2 3834	. . . . . . . . . 10
17		inss2 3834	. . . . . . . . . . . . 13
18	17	sseli 3599	. . . . . . . . . . . 12
19		elsni 4194	. . . . . . . . . . . 12
20	18, 19	syl 17	. . . . . . . . . . 11
21		0ss 3972	. . . . . . . . . . 11
22	20, 21	syl6eqss 3655	. . . . . . . . . 10
23	16, 22	syl5ss 3614	. . . . . . . . 9
24	23	rgen 2922	. . . . . . . 8
25		ralunb 3794	. . . . . . . 8 $\$ $/\$ $\$
26	24, 25	mpbiran 953	. . . . . . 7 $\$ $\$
27		inundif 4046	. . . . . . . 8 $\$
28	27	raleqi 3142	. . . . . . 7 $\$
29	15, 26, 28	3bitr2i 288	. . . . . 6 $\$ $\$
30	29	ralbii 2980	. . . . 5 $\$ $\$ $\$ $\$
31		inss1 3833	. . . . . . . . 9
32	17	sseli 3599	. . . . . . . . . . 11
33		elsni 4194	. . . . . . . . . . 11
34	32, 33	syl 17	. . . . . . . . . 10
35	34, 21	syl6eqss 3655	. . . . . . . . 9
36	31, 35	syl5ss 3614	. . . . . . . 8
37	36	ralrimivw 2967	. . . . . . 7
38	37	rgen 2922	. . . . . 6
39		ralunb 3794	. . . . . 6 $\$ $/\$ $\$
40	38, 39	mpbiran 953	. . . . 5 $\$ $\$
41	27	raleqi 3142	. . . . 5 $\$
42	30, 40, 41	3bitr2i 288	. . . 4 $\$ $\$ $\$
43	42	a1i 11	. . 3 $\$ $\$ $\$
44		difexg 4808	. . . 4 $\$
45		isbasisg 20751	. . . 4 $\$ $\$ $\$ $\$ $\$
46	44, 45	syl 17	. . 3 $\$ $\$ $\$ $\$
47		isbasisg 20751	. . 3
48	43, 46, 47	3bitr4d 300	. 2 $\$
49	8, 9, 48	pm5.21nii 368	1 $\$

Colors of variables: wff setvar class

Syntax hints:

wb 196

wceq 1483

wcel 1990

wral 2912

cvv 3200 $\$ cdif 3571

cun 3572

cin 3573

wss 3574

c0 3915

cpw 4158

csn 4177

cuni 4436

ctb 20749

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-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 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-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-sn 4178 df-pr 4180 df-uni 4437 df-bases 20750

This theorem is referenced by: (None)

W3C validator