Theorem relcnvfld

Description: if R is a relation, its double union equals the double union of its converse. (Contributed by FL, 5-Jan-2009)

	Ref	Expression
Assertion	relcnvfld	⊢ ( Rel 𝑅 → ∪ ∪ 𝑅 = ∪ ∪ ◡ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		relfld	⊢ ( Rel 𝑅 → ∪ ∪ 𝑅 = ( dom 𝑅 ∪ ran 𝑅 ) )
2		unidmrn	⊢ ∪ ∪ ◡ 𝑅 = ( dom 𝑅 ∪ ran 𝑅 )
3	1 2	eqtr4di	⊢ ( Rel 𝑅 → ∪ ∪ 𝑅 = ∪ ∪ ◡ 𝑅 )