Metamath Proof Explorer


Theorem sbthb

Description: Schroeder-Bernstein Theorem and its converse. (Contributed by NM, 8-Jun-1998)

Ref Expression
Assertion sbthb A B B A A B

Proof

Step Hyp Ref Expression
1 sbth A B B A A B
2 endom A B A B
3 ensym A B B A
4 endom B A B A
5 3 4 syl A B B A
6 2 5 jca A B A B B A
7 1 6 impbii A B B A A B