Description: Schroeder-Bernstein Theorem in class form. (Contributed by NM, 28-Mar-1998)
Ref | Expression | ||
---|---|---|---|
Assertion | sbthcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relen | |
|
2 | inss1 | |
|
3 | reldom | |
|
4 | relss | |
|
5 | 2 3 4 | mp2 | |
6 | brin | |
|
7 | vex | |
|
8 | vex | |
|
9 | 7 8 | brcnv | |
10 | 9 | anbi2i | |
11 | sbthb | |
|
12 | 6 10 11 | 3bitrri | |
13 | 1 5 12 | eqbrriv | |