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	$$⊢\mathrm{ran}\left(A\setminus {A^{-1}}^{-1}\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		dmnonrel	$$⊢\mathrm{dom}\left(A\setminus {A^{-1}}^{-1}\right)=\varnothing$$
2		dm0rn0	$$⊢\mathrm{dom}\left(A\setminus {A^{-1}}^{-1}\right)=\varnothing \leftrightarrow \mathrm{ran}\left(A\setminus {A^{-1}}^{-1}\right)=\varnothing$$
3	1 2	mpbi	$$⊢\mathrm{ran}\left(A\setminus {A^{-1}}^{-1}\right)=\varnothing$$