Metamath Proof Explorer


Theorem sbthcl

Description: Schroeder-Bernstein Theorem in class form. (Contributed by NM, 28-Mar-1998)

Ref Expression
Assertion sbthcl =-1

Proof

Step Hyp Ref Expression
1 relen Rel
2 inss1 -1
3 reldom Rel
4 relss -1RelRel-1
5 2 3 4 mp2 Rel-1
6 brin x-1yxyx-1y
7 vex xV
8 vex yV
9 7 8 brcnv x-1yyx
10 9 anbi2i xyx-1yxyyx
11 sbthb xyyxxy
12 6 10 11 3bitrri xyx-1y
13 1 5 12 eqbrriv =-1