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	|- ( ( A \ `' `' A ) |` B ) = (/)

Proof

Step	Hyp	Ref	Expression
1		ssv	|- B C_ _V
2		ssres2	|- ( B C_ _V -> ( ( A \ `' `' A ) |` B ) C_ ( ( A \ `' `' A ) |` _V ) )
3	1 2	ax-mp	|- ( ( A \ `' `' A ) |` B ) C_ ( ( A \ `' `' A ) |` _V )
4		cnvnonrel	|- `' ( A \ `' `' A ) = (/)
5	4	cnveqi	|- `' `' ( A \ `' `' A ) = `' (/)
6		cnvcnv2	|- `' `' ( A \ `' `' A ) = ( ( A \ `' `' A ) |` _V )
7		cnv0	|- `' (/) = (/)
8	5 6 7	3eqtr3i	|- ( ( A \ `' `' A ) |` _V ) = (/)
9	3 8	sseqtri	|- ( ( A \ `' `' A ) |` B ) C_ (/)
10		ss0b	|- ( ( ( A \ `' `' A ) |` B ) C_ (/) <-> ( ( A \ `' `' A ) |` B ) = (/) )
11	9 10	mpbi	|- ( ( A \ `' `' A ) |` B ) = (/)