Theorem fvnonrel

Description: The function value of any class under a non-relation is empty. (Contributed by RP, 23-Oct-2020)

	Ref	Expression
Assertion	fvnonrel	$$⊢\left(A\setminus {A^{-1}}^{-1}\right)\left(X\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		fvrn0	$$⊢\left(A\setminus {A^{-1}}^{-1}\right)\left(X\right)\in \left(\mathrm{ran}\left(A\setminus {A^{-1}}^{-1}\right)\cup \left\{\varnothing \right\}\right)$$
2		rnnonrel	$$⊢\mathrm{ran}\left(A\setminus {A^{-1}}^{-1}\right)=\varnothing$$
3		0ss	$$⊢\varnothing \subseteq \left\{\varnothing \right\}$$
4	2 3	eqsstri	$$⊢\mathrm{ran}\left(A\setminus {A^{-1}}^{-1}\right)\subseteq \left\{\varnothing \right\}$$
5		ssequn1	$$⊢\mathrm{ran}\left(A\setminus {A^{-1}}^{-1}\right)\subseteq \left\{\varnothing \right\}\leftrightarrow \mathrm{ran}\left(A\setminus {A^{-1}}^{-1}\right)\cup \left\{\varnothing \right\}=\left\{\varnothing \right\}$$
6	4 5	mpbi	$$⊢\mathrm{ran}\left(A\setminus {A^{-1}}^{-1}\right)\cup \left\{\varnothing \right\}=\left\{\varnothing \right\}$$
7	1 6	eleqtri	$$⊢\left(A\setminus {A^{-1}}^{-1}\right)\left(X\right)\in \left\{\varnothing \right\}$$
8		fvex	$$⊢\left(A\setminus {A^{-1}}^{-1}\right)\left(X\right)\in \mathrm{V}$$
9	8	elsn	$$⊢\left(A\setminus {A^{-1}}^{-1}\right)\left(X\right)\in \left\{\varnothing \right\}\leftrightarrow \left(A\setminus {A^{-1}}^{-1}\right)\left(X\right)=\varnothing$$
10	7 9	mpbi	$$⊢\left(A\setminus {A^{-1}}^{-1}\right)\left(X\right)=\varnothing$$