Metamath Proof Explorer

Theorem relrngo

Description: Obsolete theorem. 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.) (Proof modification is discouraged.)

Ref Expression
Assertion relrngo ⊢ Rel ⁡ RingOps

Proof

Step Hyp Ref Expression
1 df-rngo ⊢ RingOps = g h | g ∈ AbelOp ∧ h : ran ⁡ g × ran ⁡ g ⟶ ran ⁡ g ∧ ∀ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g ∀ z ∈ ran ⁡ g x h y h z = x h y h z ∧ x h y g z = x h y g x h z ∧ x g y h z = x h z g y h z ∧ ∃ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g x h y = y ∧ y h x = y
2 1 relopabiv ⊢ Rel ⁡ RingOps