Theorem co01

Description: Composition with the empty set. (Contributed by NM, 24-Apr-2004)

	Ref	Expression
Assertion	co01	|- ( (/) o. A ) = (/)

Proof

Step	Hyp	Ref	Expression
1		cnv0	|- `' (/) = (/)
2		cnvco	|- `' ( (/) o. A ) = ( `' A o. `' (/) )
3	1	coeq2i	|- ( `' A o. `' (/) ) = ( `' A o. (/) )
4		co02	|- ( `' A o. (/) ) = (/)
5	2 3 4	3eqtri	|- `' ( (/) o. A ) = (/)
6	1 5	eqtr4i	|- `' (/) = `' ( (/) o. A )
7	6	cnveqi	|- `' `' (/) = `' `' ( (/) o. A )
8		rel0	|- Rel (/)
9		dfrel2	|- ( Rel (/) <-> `' `' (/) = (/) )
10	8 9	mpbi	|- `' `' (/) = (/)
11		relco	|- Rel ( (/) o. A )
12		dfrel2	|- ( Rel ( (/) o. A ) <-> `' `' ( (/) o. A ) = ( (/) o. A ) )
13	11 12	mpbi	|- `' `' ( (/) o. A ) = ( (/) o. A )
14	7 10 13	3eqtr3ri	|- ( (/) o. A ) = (/)