Metamath Proof Explorer


Theorem rimf1o

Description: An isomorphism of rings is a bijection. (Contributed by AV, 22-Oct-2019)

Ref Expression
Hypotheses rhmf1o.b B = Base R
rhmf1o.c C = Base S
Assertion rimf1o F R RingIso S F : B 1-1 onto C

Proof

Step Hyp Ref Expression
1 rhmf1o.b B = Base R
2 rhmf1o.c C = Base S
3 1 2 isrim F R RingIso S F R RingHom S F : B 1-1 onto C
4 3 simprbi F R RingIso S F : B 1-1 onto C