Theorem co02 6262

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 6110	. 2 ⊢ Rel (𝐴 ∘ ∅)
2		rel0 5785	. 2 ⊢ Rel ∅
3		br0 5160	. . . . . 6 ⊢ ¬ 𝑥∅𝑧
4	3	intnanr 492	. . . . 5 ⊢ ¬ (𝑥∅𝑧 ∧ 𝑧𝐴𝑦)
5	4	nex 1830	. . . 4 ⊢ ¬ ∃𝑧(𝑥∅𝑧 ∧ 𝑧𝐴𝑦)
6		vex 3459	. . . . 5 ⊢ 𝑥 ∈ V
7		vex 3459	. . . . 5 ⊢ 𝑦 ∈ V
8	6, 7	opelco 5857	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ ∅) ↔ ∃𝑧(𝑥∅𝑧 ∧ 𝑧𝐴𝑦))
9	5, 8	mtbir 326	. . 3 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ ∅)
10		noel 4291	. . 3 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
11	9, 10	2false 378	. 2 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ ∅) ↔ ⟨𝑥, 𝑦⟩ ∈ ∅)
12	1, 2, 11	eqrelriiv 5776	1 ⊢ (𝐴 ∘ ∅) = ∅

Syntax hints:   ∧ wa 400   = wceq 1570  ∃wex 1809   ∈ wcel 2143  ∅c0 4286  ⟨cop 4595   class class class wbr 5109   ∘ ccom 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-xp 5667  df-rel 5668  df-co 5670

This theorem is referenced by:  co01  6263  dfpo2  6297  relexpsucld  15067  gsumwmhm  18899  frmdgsum  18916  frmdup1  18918  efginvrel2  19792  0frgp  19844  evl1fval  22488  utop2nei  24407  tngds  24805  tocycf  33437  tocyc01  33438  1arithidom  33827  mrsub0  36008  cononrel1  44320