Theorem sdomen2

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

	Ref	Expression
Assertion	sdomen2	⊢ ( 𝐴 ≈ 𝐵 → ( 𝐶 ≺ 𝐴 ↔ 𝐶 ≺ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		sdomentr	⊢ ( ( 𝐶 ≺ 𝐴 ∧ 𝐴 ≈ 𝐵 ) → 𝐶 ≺ 𝐵 )
2	1	ancoms	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≺ 𝐴 ) → 𝐶 ≺ 𝐵 )
3		ensym	⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴 )
4		sdomentr	⊢ ( ( 𝐶 ≺ 𝐵 ∧ 𝐵 ≈ 𝐴 ) → 𝐶 ≺ 𝐴 )
5	4	ancoms	⊢ ( ( 𝐵 ≈ 𝐴 ∧ 𝐶 ≺ 𝐵 ) → 𝐶 ≺ 𝐴 )
6	3 5	sylan	⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐶 ≺ 𝐵 ) → 𝐶 ≺ 𝐴 )
7	2 6	impbida	⊢ ( 𝐴 ≈ 𝐵 → ( 𝐶 ≺ 𝐴 ↔ 𝐶 ≺ 𝐵 ) )