Metamath Proof Explorer

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 
|- ( R ~=r S -> ( R e. Domn <-> S e. Domn ) )

Proof

Step Hyp Ref Expression
1 ricdomn1 
 |-  ( ( R ~=r S /\ R e. Domn ) -> S e. Domn )
2 ricsym 
 |-  ( R ~=r S -> S ~=r R )
3 ricdomn1 
 |-  ( ( S ~=r R /\ S e. Domn ) -> R e. Domn )
4 2 3 sylan 
 |-  ( ( R ~=r S /\ S e. Domn ) -> R e. Domn )
5 1 4 impbida 
 |-  ( R ~=r S -> ( R e. Domn <-> S e. Domn ) )