Theorem sdomen1

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

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

Proof

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