# Metamath Proof Explorer

## 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)↾}_{{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)↾}_{{B}}\subseteq {\left({A}\setminus {{{A}}^{-1}}^{-1}\right)↾}_{\mathrm{V}}$
3 1 2 ax-mp ${⊢}{\left({A}\setminus {{{A}}^{-1}}^{-1}\right)↾}_{{B}}\subseteq {\left({A}\setminus {{{A}}^{-1}}^{-1}\right)↾}_{\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)↾}_{\mathrm{V}}$
7 cnv0 ${⊢}{\varnothing }^{-1}=\varnothing$
8 5 6 7 3eqtr3i ${⊢}{\left({A}\setminus {{{A}}^{-1}}^{-1}\right)↾}_{\mathrm{V}}=\varnothing$
9 3 8 sseqtri ${⊢}{\left({A}\setminus {{{A}}^{-1}}^{-1}\right)↾}_{{B}}\subseteq \varnothing$
10 ss0b ${⊢}{\left({A}\setminus {{{A}}^{-1}}^{-1}\right)↾}_{{B}}\subseteq \varnothing ↔{\left({A}\setminus {{{A}}^{-1}}^{-1}\right)↾}_{{B}}=\varnothing$
11 9 10 mpbi ${⊢}{\left({A}\setminus {{{A}}^{-1}}^{-1}\right)↾}_{{B}}=\varnothing$