Theorem dfrn6

Description: Alternate definition of range. (Contributed by Peter Mazsa, 1-Aug-2018)

	Ref	Expression
Assertion	dfrn6	⊢ ran 𝑅 = { 𝑥 ∣ [ 𝑥 ] ◡ 𝑅 ≠ ∅ }

Proof

Step	Hyp	Ref	Expression
1		df-rn	⊢ ran 𝑅 = dom ◡ 𝑅
2		dfdm6	⊢ dom ◡ 𝑅 = { 𝑥 ∣ [ 𝑥 ] ◡ 𝑅 ≠ ∅ }
3	1 2	eqtri	⊢ ran 𝑅 = { 𝑥 ∣ [ 𝑥 ] ◡ 𝑅 ≠ ∅ }