Theorem dfcoss4

Description: Alternate definition of the class of cosets by R (see the comment of df-coss ). (Contributed by Peter Mazsa, 12-Jul-2021)

	Ref	Expression
Assertion	dfcoss4	⊢ ≀ 𝑅 = ran ( 𝑅 ⋉ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		df-coss	⊢ ≀ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) }
2		rnxrn	⊢ ran ( 𝑅 ⋉ 𝑅 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) }
3	1 2	eqtr4i	⊢ ≀ 𝑅 = ran ( 𝑅 ⋉ 𝑅 )