co02 - Metamath Proof Explorer

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

Theorem co02 5348

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 5333	. 2
2		rel0 4960	. 2
3		noel 3638	. . . . . . 7
4		df-br 4290	. . . . . . 7
5	3, 4	mtbir 299	. . . . . 6
6	5	intnanr 901	. . . . 5 $/\$
7	6	nex 1605	. . . 4 $/\$
8		vex 2973	. . . . 5
9		vex 2973	. . . . 5
10	8, 9	opelco 5007	. . . 4 $/\$
11	7, 10	mtbir 299	. . 3
12		noel 3638	. . 3
13	11, 12	2false 350	. 2
14	1, 2, 13	eqrelriiv 4930	1

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 369

wceq 1364

wex 1591

wcel 1761

c0 3634

cop 3880 class class class wbr 4289

ccom 4840

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-sep 4410 ax-nul 4418 ax-pr 4528

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2263 df-mo 2264 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-ral 2718 df-rex 2719 df-rab 2722 df-v 2972 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-nul 3635 df-if 3789 df-sn 3875 df-pr 3877 df-op 3881 df-br 4290 df-opab 4348 df-xp 4842 df-rel 4843 df-co 4845

This theorem is referenced by: co01 5349 gsumwmhm 15516 frmdgsum 15533 frmdup1 15535 efginvrel2 16217 0frgp 16269 ust0 19694 utop2nei 19725 tngds 20134 evl1fval 21436 dfpo2 27478