Theorem ricdomn

Description: A ring is a domain if and only if an isomorphic ring is a domain. (Contributed by Thierry Arnoux, 4-May-2026)

	Ref	Expression
Assertion	ricdomn	⊢ ( 𝑅 ≃𝑟 𝑆 → ( 𝑅 ∈ Domn ↔ 𝑆 ∈ Domn ) )

Proof

Step	Hyp	Ref	Expression
1		ricdomn1	⊢ ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ Domn ) → 𝑆 ∈ Domn )
2		ricsym	⊢ ( 𝑅 ≃𝑟 𝑆 → 𝑆 ≃𝑟 𝑅 )
3		ricdomn1	⊢ ( ( 𝑆 ≃𝑟 𝑅 ∧ 𝑆 ∈ Domn ) → 𝑅 ∈ Domn )
4	2 3	sylan	⊢ ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑆 ∈ Domn ) → 𝑅 ∈ Domn )
5	1 4	impbida	⊢ ( 𝑅 ≃𝑟 𝑆 → ( 𝑅 ∈ Domn ↔ 𝑆 ∈ Domn ) )