co02 - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > co02		Structured version Unicode version

Theorem co02 5520

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

**Assertion**
Ref	Expression
co02

Proof of Theorem co02 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relco 5504	. 2
2		rel0 5126	. 2
3		noel 3789	. . . . . . 7
4		df-br 4448	. . . . . . 7
5	3, 4	mtbir 299	. . . . . 6
6	5	intnanr 913	. . . . 5 $/\$
7	6	nex 1610	. . . 4 $/\$
8		vex 3116	. . . . 5
9		vex 3116	. . . . 5
10	8, 9	opelco 5173	. . . 4 $/\$
11	7, 10	mtbir 299	. . 3
12		noel 3789	. . 3
13	11, 12	2false 350	. 2
14	1, 2, 13	eqrelriiv 5096	1

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 369

wceq 1379

wex 1596

wcel 1767

c0 3785

cop 4033 class class class wbr 4447

ccom 5003

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4568 ax-nul 4576 ax-pr 4686

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-ral 2819 df-rex 2820 df-rab 2823 df-v 3115 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-nul 3786 df-if 3940 df-sn 4028 df-pr 4030 df-op 4034 df-br 4448 df-opab 4506 df-xp 5005 df-rel 5006 df-co 5008

This theorem is referenced by: co01 5521 gsumwmhm 15842 frmdgsum 15859 frmdup1 15861 efginvrel2 16548 0frgp 16600 evl1fval 18151 ust0 20473 utop2nei 20504 tngds 20913 dfpo2 28777