Theorem co02

Description: Composition with the empty set. Theorem 20 of Suppes p. 63. (Contributed by NM, 24-Apr-2004)

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

Proof

Step	Hyp	Ref	Expression
1		relco	|- Rel ( A o. (/) )
2		rel0	|- Rel (/)
3		br0	|- -. x (/) z
4	3	intnanr	|- -. ( x (/) z /\ z A y )
5	4	nex	|- -. E. z ( x (/) z /\ z A y )
6		vex	|- x e. _V
7		vex	|- y e. _V
8	6 7	opelco	|- ( <. x , y >. e. ( A o. (/) ) <-> E. z ( x (/) z /\ z A y ) )
9	5 8	mtbir	|- -. <. x , y >. e. ( A o. (/) )
10		noel	|- -. <. x , y >. e. (/)
11	9 10	2false	|- ( <. x , y >. e. ( A o. (/) ) <-> <. x , y >. e. (/) )
12	1 2 11	eqrelriiv	|- ( A o. (/) ) = (/)