Theorem rnco2 6257

Description: The range of the composition of two classes. (Contributed by NM, 27-Mar-2008.)

Assertion

Ref	Expression
rnco2	⊢ ran (𝐴 ∘ 𝐵) = (𝐴 “ ran 𝐵)

Proof of Theorem rnco2

Step	Hyp	Ref	Expression
1		rnco 6255	. 2 ⊢ ran (𝐴 ∘ 𝐵) = ran (𝐴 ↾ ran 𝐵)
2		df-ima 5663	. 2 ⊢ (𝐴 “ ran 𝐵) = ran (𝐴 ↾ ran 𝐵)
3	1, 2	eqtr4i 2786	1 ⊢ ran (𝐴 ∘ 𝐵) = (𝐴 “ ran 𝐵)

This proof depends on syntax axioms:   = wceq 1569  ran crn 5651   ↾ cres 5652   “ cima 5653   ∘ ccom 5654

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5656  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663

This theorem is used by:  dmco  6258  isf34lem7  10462  isf34lem6  10463  imasless  17719  gsumzf1o  20133  gsumzmhm  20158  gsumzinv  20166  dprdf1o  20255  pf1rcl  22674  ovolficcss  25797  volsup  25884  uniiccdif  25906  uniioombllem3  25913  dyadmbl  25928  itg1climres  26042  acwer1prc  35818  cvmlift3lem6  36177  mblfinlem2  38683  volsupnfl  38690