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 )