Theorem sdomen1

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

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

Proof

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