# Metamath Proof Explorer

## Theorem relrngo

Description: The class of all unital rings is a relation. (Contributed by FL, 31-Aug-2009) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion relrngo ${⊢}\mathrm{Rel}\mathrm{RingOps}$

### Proof

Step Hyp Ref Expression
1 df-rngo ${⊢}\mathrm{RingOps}=\left\{⟨{g},{h}⟩|\left(\left({g}\in \mathrm{AbelOp}\wedge {h}:\mathrm{ran}{g}×\mathrm{ran}{g}⟶\mathrm{ran}{g}\right)\wedge \left(\forall {x}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\left(\left({x}{h}{y}\right){h}{z}={x}{h}\left({y}{h}{z}\right)\wedge {x}{h}\left({y}{g}{z}\right)=\left({x}{h}{y}\right){g}\left({x}{h}{z}\right)\wedge \left({x}{g}{y}\right){h}{z}=\left({x}{h}{z}\right){g}\left({y}{h}{z}\right)\right)\wedge \exists {x}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{g}\phantom{\rule{.4em}{0ex}}\left({x}{h}{y}={y}\wedge {y}{h}{x}={y}\right)\right)\right)\right\}$
2 1 relopabi ${⊢}\mathrm{Rel}\mathrm{RingOps}$