sbthlem1 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem sbthlem1 4447

Description: Lemma for sbth 4457.

**Hypotheses**
Ref	Expression
sbthlem.1
sbthlem.2	$/\$

**Assertion**
Ref	Expression
sbthlem1

**Proof of Theorem sbthlem1**
Step	Hyp	Ref	Expression
1		unissb 2528	. 2
2		sbthlem.2	. . . . 5 $/\$
3	2	abeq2i 1570	. . . 4 $/\$
4		ssconb 2170	. . . . . . . . 9 $/\$
5	4	biimprd 154	. . . . . . . 8 $/\$
6	5	ex 373	. . . . . . 7
7		difss 2167	. . . . . . . 8
8		sstr2 2071	. . . . . . . 8
9	7, 8	mpi 44	. . . . . . 7
10	6, 9	syl5 21	. . . . . 6
11	10	pm2.43d 65	. . . . 5
12	11	imp 350	. . . 4 $/\$
13	3, 12	sylbi 199	. . 3
14		elssuni 2526	. . . . 5
15		imass2 3433	. . . . 5
16		sscon 2171	. . . . 5
17	14, 15, 16	3syl 20	. . . 4
18		imass2 3433	. . . 4
19		sscon 2171	. . . 4
20	17, 18, 19	3syl 20	. . 3
21	13, 20	sstrd 2074	. 2
22	1, 21	mprgbir 1701	1

Colors of variables: wff set class

Syntax hints:

wi 3 $/\$ wa 223

wceq 956

wcel 958

cab 1463

cvv 1811

cdif 2044

wss 2047

cuni 2503

cima 3173

This theorem is referenced by: sbthlem2 4448 sbthlem3 4449 sbthlem5 4451

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 962 ax-gen 963 ax-8 964 ax-10 966 ax-11 967 ax-12 968 ax-13 969 ax-14 970 ax-17 971 ax-4 973 ax-5o 975 ax-6o 978 ax-9o 1123 ax-10o 1140 ax-16 1210 ax-11o 1218 ax-ext 1459 ax-sep 2703 ax-pow 2742 ax-pr 2779

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 981 df-sb 1172 df-eu 1382 df-mo 1383 df-clab 1464 df-cleq 1469 df-clel 1472 df-ne 1587 df-ral 1649 df-v 1812 df-dif 2049 df-un 2050 df-in 2051 df-ss 2053 df-nul 2281 df-pw 2402 df-sn 2412 df-pr 2413 df-op 2416 df-uni 2504 df-br 2620 df-opab 2667 df-xp 3184 df-rel 3185 df-cnv 3186 df-dm 3188 df-rn 3189 df-res 3190 df-ima 3191