Theorem co02 6227

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 6075	. 2 ⊢ Rel (𝐴 ∘ ∅)
2		rel0 5756	. 2 ⊢ Rel ∅
3		br0 5149	. . . . . 6 ⊢ ¬ 𝑥∅𝑧
4	3	intnanr 487	. . . . 5 ⊢ ¬ (𝑥∅𝑧 ∧ 𝑧𝐴𝑦)
5	4	nex 1802	. . . 4 ⊢ ¬ ∃𝑧(𝑥∅𝑧 ∧ 𝑧𝐴𝑦)
6		vex 3446	. . . . 5 ⊢ 𝑥 ∈ V
7		vex 3446	. . . . 5 ⊢ 𝑦 ∈ V
8	6, 7	opelco 5828	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ ∅) ↔ ∃𝑧(𝑥∅𝑧 ∧ 𝑧𝐴𝑦))
9	5, 8	mtbir 323	. . 3 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ ∅)
10		noel 4292	. . 3 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
11	9, 10	2false 375	. 2 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ ∅) ↔ ⟨𝑥, 𝑦⟩ ∈ ∅)
12	1, 2, 11	eqrelriiv 5747	1 ⊢ (𝐴 ∘ ∅) = ∅

Syntax hints:   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∅c0 4287  ⟨cop 4588   class class class wbr 5100   ∘ ccom 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-rel 5639  df-co 5641

This theorem is referenced by:  co01  6228  dfpo2  6262  relexpsucld  14969  gsumwmhm  18782  frmdgsum  18799  frmdup1  18801  efginvrel2  19668  0frgp  19720  evl1fval  22284  utop2nei  24206  tngds  24604  tocycf  33211  tocyc01  33212  1arithidom  33630  mrsub0  35732  cononrel1  43950