sbthlem1 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem sbthlem1 4433

Description: Lemma for sbth 4443.

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

**Assertion**
Ref	Expression
sbthlem1

**Proof of Theorem sbthlem1**
Step	Hyp	Ref	Expression
1		unissb 2523	. 2
2		sbthlem.2	. . . . 5 $/\$
3	2	abeq2i 1567	. . . 4 $/\$
4		ssconb 2166	. . . . . . . . 9 $/\$
5	4	biimprd 154	. . . . . . . 8 $/\$
6	5	ex 373	. . . . . . 7
7		difss 2163	. . . . . . . 8
8		sstr2 2067	. . . . . . . 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 2521	. . . . 5
15		imass2 3425	. . . . 5
16		sscon 2167	. . . . 5
17	14, 15, 16	3syl 20	. . . 4
18		imass2 3425	. . . 4
19		sscon 2167	. . . 4
20	17, 18, 19	3syl 20	. . 3
21	13, 20	sstrd 2070	. 2
22	1, 21	mprgbir 1698	1

Colors of variables: wff set class

Syntax hints:

wi 3 $/\$ wa 223

wceq 954

wcel 956

cab 1461

cvv 1807

cdif 2040

wss 2043

cuni 2498

cima 3168

This theorem is referenced by: sbthlem2 4434 sbthlem3 4435 sbthlem5 4437

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 960 ax-gen 961 ax-8 962 ax-10 964 ax-11 965 ax-12 966 ax-13 967 ax-14 968 ax-17 969 ax-4 971 ax-5o 973 ax-6o 976 ax-9o 1121 ax-10o 1138 ax-16 1208 ax-11o 1216 ax-ext 1457 ax-sep 2698 ax-pow 2737 ax-pr 2774

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 979 df-sb 1170 df-eu 1380 df-mo 1381 df-clab 1462 df-cleq 1467 df-clel 1470 df-ne 1584 df-ral 1646 df-v 1808 df-dif 2045 df-un 2046 df-in 2047 df-ss 2049 df-nul 2277 df-pw 2398 df-sn 2408 df-pr 2409 df-op 2412 df-uni 2499 df-br 2615 df-opab 2662 df-xp 3179 df-rel 3180 df-cnv 3181 df-dm 3183 df-rn 3184 df-res 3185 df-ima 3186