Theorem domen2

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

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

Proof

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