Theorem cononrel1

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

	Ref	Expression
Assertion	cononrel1	|- ( ( A \ `' `' A ) o. B ) = (/)

Proof

Step	Hyp	Ref	Expression
1		cnvco	|- `' ( ( A \ `' `' A ) o. B ) = ( `' B o. `' ( A \ `' `' A ) )
2		cnvnonrel	|- `' ( A \ `' `' A ) = (/)
3	2	coeq2i	|- ( `' B o. `' ( A \ `' `' A ) ) = ( `' B o. (/) )
4		co02	|- ( `' B o. (/) ) = (/)
5	1 3 4	3eqtri	|- `' ( ( A \ `' `' A ) o. B ) = (/)
6	5	cnveqi	|- `' `' ( ( A \ `' `' A ) o. B ) = `' (/)
7		relco	|- Rel ( ( A \ `' `' A ) o. B )
8		dfrel2	|- ( Rel ( ( A \ `' `' A ) o. B ) <-> `' `' ( ( A \ `' `' A ) o. B ) = ( ( A \ `' `' A ) o. B ) )
9	7 8	mpbi	|- `' `' ( ( A \ `' `' A ) o. B ) = ( ( A \ `' `' A ) o. B )
10		cnv0	|- `' (/) = (/)
11	6 9 10	3eqtr3i	|- ( ( A \ `' `' A ) o. B ) = (/)