Theorem resnonrel

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

	Ref	Expression
Assertion	resnonrel	$$⊢{\left(A\setminus {A^{-1}}^{-1}\right)\upharpoonright }_B=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		ssv	$$⊢B\subseteq \mathrm{V}$$
2		ssres2	$$⊢B\subseteq \mathrm{V}\to {\left(A\setminus {A^{-1}}^{-1}\right)\upharpoonright }_B\subseteq {\left(A\setminus {A^{-1}}^{-1}\right)\upharpoonright }_{\mathrm{V}}$$
3	1 2	ax-mp	$$⊢{\left(A\setminus {A^{-1}}^{-1}\right)\upharpoonright }_B\subseteq {\left(A\setminus {A^{-1}}^{-1}\right)\upharpoonright }_{\mathrm{V}}$$
4		cnvnonrel	$$⊢{\left(A\setminus {A^{-1}}^{-1}\right)}^{-1}=\varnothing$$
5	4	cnveqi	$$⊢{{\left(A\setminus {A^{-1}}^{-1}\right)}^{-1}}^{-1}={\varnothing }^{-1}$$
6		cnvcnv2	$$⊢{{\left(A\setminus {A^{-1}}^{-1}\right)}^{-1}}^{-1}={\left(A\setminus {A^{-1}}^{-1}\right)\upharpoonright }_{\mathrm{V}}$$
7		cnv0	$$⊢{\varnothing }^{-1}=\varnothing$$
8	5 6 7	3eqtr3i	$$⊢{\left(A\setminus {A^{-1}}^{-1}\right)\upharpoonright }_{\mathrm{V}}=\varnothing$$
9	3 8	sseqtri	$$⊢{\left(A\setminus {A^{-1}}^{-1}\right)\upharpoonright }_B\subseteq \varnothing$$
10		ss0b	$$⊢{\left(A\setminus {A^{-1}}^{-1}\right)\upharpoonright }_B\subseteq \varnothing \leftrightarrow {\left(A\setminus {A^{-1}}^{-1}\right)\upharpoonright }_B=\varnothing$$
11	9 10	mpbi	$$⊢{\left(A\setminus {A^{-1}}^{-1}\right)\upharpoonright }_B=\varnothing$$