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	⊢ Rel RingOps

Proof

Step	Hyp	Ref	Expression
1		df-rngo	⊢ RingOps = { ⟨ 𝑔 , ℎ ⟩ ∣ ( ( 𝑔 ∈ AbelOp ∧ ℎ : ( ran 𝑔 × ran 𝑔 ) ⟶ ran 𝑔 ) ∧ ( ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ∀ 𝑧 ∈ ran 𝑔 ( ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 ) = ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) ) ∧ ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) ) = ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) ) ∧ ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑥 ℎ 𝑦 ) = 𝑦 ∧ ( 𝑦 ℎ 𝑥 ) = 𝑦 ) ) ) }
2	1	relopabiv	⊢ Rel RingOps