This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbthb

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

		Ref	Expression
	Assertion	sbthb	$⊢ (A ≼ B \land B ≼ A) \leftrightarrow A \approx B$

Step	Hyp	Ref	Expression
1		sbth	$⊢ (A ≼ B \land B ≼ A) \to A \approx B$
2		endom	$⊢ A \approx B \to A ≼ B$
3		ensym	$⊢ A \approx B \to B \approx A$
4		endom	$⊢ B \approx A \to B ≼ A$
5	3 4	syl	$⊢ A \approx B \to B ≼ A$
6	2 5	jca	$⊢ A \approx B \to (A ≼ B \land B ≼ A)$
7	1 6	impbii	$⊢ (A ≼ B \land B ≼ A) \leftrightarrow A \approx B$