Theorem brric2

Description: The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011) (Revised by AV, 23-Jul-2026)

	Ref	Expression
Assertion	brric2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) → ( 𝑅 ≃𝑟 𝑆 ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isbrric2	⊢ ( 𝑅 ≃𝑟 𝑆 ↔ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ) )
2	1	baib	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) → ( 𝑅 ≃𝑟 𝑆 ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ) )