Theorem rnnonrel

Description: The range of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020)

	Ref	Expression
Assertion	rnnonrel	⊢ ran ( 𝐴 ∖ ◡ ◡ 𝐴 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		dmnonrel	⊢ dom ( 𝐴 ∖ ◡ ◡ 𝐴 ) = ∅
2		dm0rn0	⊢ ( dom ( 𝐴 ∖ ◡ ◡ 𝐴 ) = ∅ ↔ ran ( 𝐴 ∖ ◡ ◡ 𝐴 ) = ∅ )
3	1 2	mpbi	⊢ ran ( 𝐴 ∖ ◡ ◡ 𝐴 ) = ∅