Theorem sdomen2

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

	Ref	Expression
Assertion	sdomen2	$$⊢A\approx B\to \left(C\prec A\leftrightarrow C\prec B\right)$$

Proof

Step	Hyp	Ref	Expression
1		sdomentr	$$⊢\left(C\prec A\wedge A\approx B\right)\to C\prec B$$
2	1	ancoms	$$⊢\left(A\approx B\wedge C\prec A\right)\to C\prec B$$
3		ensym	$$⊢A\approx B\to B\approx A$$
4		sdomentr	$$⊢\left(C\prec B\wedge B\approx A\right)\to C\prec A$$
5	4	ancoms	$$⊢\left(B\approx A\wedge C\prec B\right)\to C\prec A$$
6	3 5	sylan	$$⊢\left(A\approx B\wedge C\prec B\right)\to C\prec A$$
7	2 6	impbida	$$⊢A\approx B\to \left(C\prec A\leftrightarrow C\prec B\right)$$