Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem sbthlem1 3349

Description: Lemma for Schroeder-Bernstein Theorem.

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

**Assertion**
Ref	Expression
sbthlem1

Distinct variable group(s):

**Proof of Theorem sbthlem1**
Step	Hyp	Ref	Expression
1		unissb 1941	. 2
2		sbthlem.2	. . . . 5 $/\$
3	2	cleqabi 1176	. . . 4 $/\$
4		ssconb 1598	. . . . . . . . 9 $/\$
5	4	biimprd 136	. . . . . . . 8 $/\$
6	5	exp 291	. . . . . . 7
7		difss 1596	. . . . . . . 8
8		sstr2 1510	. . . . . . . 8
9	7, 8	mpi 44	. . . . . . 7
10	6, 9	syl5 22	. . . . . 6
11	10	pm2.43d 59	. . . . 5
12	11	imp 277	. . . 4 $/\$
13	3, 12	sylbi 174	. . 3
14		elssuni 1940	. . . . 5
15		imass2 2622	. . . . 5
16		sscon 1599	. . . . 5
17	14, 15, 16	3syl 21	. . . 4
18		imass2 2622	. . . 4
19		sscon 1599	. . . 4
20	17, 18, 19	3syl 21	. . 3
21	13, 20	sstrd 1513	. 2
22	1, 21	mprgbir 1250	1

Colors of variables: wff set class

Syntax hints:

wi 2 $/\$ wa 196

cab 1090

wceq 1091

wcel 1092

cvv 1348

cdif 1484

wss 1487

cuni 1919

cima 2413

This theorem is referenced by: sbthlem2 3350 sbthlem3 3351 sbthlem5 3353

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-pow 1077

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-ex 679 df-sb 853 df-clab 1093 df-cleq 1097 df-clel 1099 df-ral 1205 df-v 1349 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-nul 1708 df-pw 1799 df-sn 1811 df-pr 1812 df-op 1815 df-uni 1920 df-br 2063 df-opab 2098 df-xp 2424 df-rel 2425 df-cnv 2426 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431