Metamath Proof Explorer

Theorem cononrel2

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

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

Proof

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