co02 - Metamath Proof Explorer

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

Theorem co02 5351

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 5336	. 2
2		rel0 4964	. 2
3		noel 3641	. . . . . . 7
4		df-br 4293	. . . . . . 7
5	3, 4	mtbir 299	. . . . . 6
6	5	intnanr 906	. . . . 5 $/\$
7	6	nex 1600	. . . 4 $/\$
8		vex 2975	. . . . 5
9		vex 2975	. . . . 5
10	8, 9	opelco 5011	. . . 4 $/\$
11	7, 10	mtbir 299	. . 3
12		noel 3641	. . 3
13	11, 12	2false 350	. 2
14	1, 2, 13	eqrelriiv 4934	1

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 369

wceq 1369

wex 1586

wcel 1756

c0 3637

cop 3883 class class class wbr 4292

ccom 4844

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-sep 4413 ax-nul 4421 ax-pr 4531

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2568 df-ne 2608 df-ral 2720 df-rex 2721 df-rab 2724 df-v 2974 df-dif 3331 df-un 3333 df-in 3335 df-ss 3342 df-nul 3638 df-if 3792 df-sn 3878 df-pr 3880 df-op 3884 df-br 4293 df-opab 4351 df-xp 4846 df-rel 4847 df-co 4849

This theorem is referenced by: co01 5352 gsumwmhm 15523 frmdgsum 15540 frmdup1 15542 efginvrel2 16224 0frgp 16276 evl1fval 17762 ust0 19794 utop2nei 19825 tngds 20234 dfpo2 27565