domen2

Description: Equality-like theorem for equinumerosity and dominance. (Contributed by NM, 8-Nov-2003)

		Ref	Expression
	Assertion	domen2	$⊢ A \approx B \to (C ≼ A \leftrightarrow C ≼ B)$

Step	Hyp	Ref	Expression
1		domentr	$⊢ (C ≼ A \land A \approx B) \to C ≼ B$
2	1	ancoms	$⊢ (A \approx B \land C ≼ A) \to C ≼ B$
3		ensym	$⊢ A \approx B \to B \approx A$
4		domentr	$⊢ (C ≼ B \land B \approx A) \to C ≼ A$
5	4	ancoms	$⊢ (B \approx A \land C ≼ B) \to C ≼ A$
6	3 5	sylan	$⊢ (A \approx B \land C ≼ B) \to C ≼ A$
7	2 6	impbida	$⊢ A \approx B \to (C ≼ A \leftrightarrow C ≼ B)$

Metamath Proof Explorer