Metamath Proof Explorer


Theorem brrici

Description: Prove isomorphic by an explicit isomorphism. (Contributed by SN, 10-Jan-2025)

Ref Expression
Assertion brrici ( 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) → 𝑅𝑟 𝑆 )

Proof

Step Hyp Ref Expression
1 ne0i ( 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) → ( 𝑅 RingIso 𝑆 ) ≠ ∅ )
2 brric ( 𝑅𝑟 𝑆 ↔ ( 𝑅 RingIso 𝑆 ) ≠ ∅ )
3 1 2 sylibr ( 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) → 𝑅𝑟 𝑆 )