Theorem co02 6212

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 6060	. 2 ⊢ Rel (𝐴 ∘ ∅)
2		rel0 5742	. 2 ⊢ Rel ∅
3		br0 5121	. . . . . 6 ⊢ ¬ 𝑥∅𝑧
4	3	intnanr 488	. . . . 5 ⊢ ¬ (𝑥∅𝑧 ∧ 𝑧𝐴𝑦)
5	4	nex 1807	. . . 4 ⊢ ¬ ∃𝑧(𝑥∅𝑧 ∧ 𝑧𝐴𝑦)
6		vex 3435	. . . . 5 ⊢ 𝑥 ∈ V
7		vex 3435	. . . . 5 ⊢ 𝑦 ∈ V
8	6, 7	opelco 5813	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ ∅) ↔ ∃𝑧(𝑥∅𝑧 ∧ 𝑧𝐴𝑦))
9	5, 8	mtbir 324	. . 3 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ ∅)
10		noel 4266	. . 3 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
11	9, 10	2false 376	. 2 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ ∅) ↔ ⟨𝑥, 𝑦⟩ ∈ ∅)
12	1, 2, 11	eqrelriiv 5733	1 ⊢ (𝐴 ∘ ∅) = ∅

Syntax hints:   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119  ∅c0 4261  ⟨cop 4561   class class class wbr 5072   ∘ ccom 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-xp 5624  df-rel 5625  df-co 5627

This theorem is referenced by:  co01  6213  dfpo2  6247  relexpsucld  14987  gsumwmhm  18804  frmdgsum  18821  frmdup1  18823  efginvrel2  19693  0frgp  19745  evl1fval  22314  utop2nei  24233  tngds  24631  tocycf  33198  tocyc01  33199  1arithidom  33620  mrsub0  35744  cononrel1  44038