Theorem rnun 6133

Description: Distributive law for range over union. Theorem 8 of [Suppes] p. 60. (Contributed by NM, 24-Mar-1998.)

Assertion

Ref	Expression
rnun	⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵)

Proof of Theorem rnun

Step	Hyp	Ref	Expression
1		cnvun 6130	. . . 4 ⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵)
2	1	dmeqi 5885	. . 3 ⊢ dom ◡(𝐴 ∪ 𝐵) = dom (◡𝐴 ∪ ◡𝐵)
3		dmun 5891	. . 3 ⊢ dom (◡𝐴 ∪ ◡𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
4	2, 3	eqtri 2788	. 2 ⊢ dom ◡(𝐴 ∪ 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
5		df-rn 5663	. 2 ⊢ ran (𝐴 ∪ 𝐵) = dom ◡(𝐴 ∪ 𝐵)
6		df-rn 5663	. . 3 ⊢ ran 𝐴 = dom ◡𝐴
7		df-rn 5663	. . 3 ⊢ ran 𝐵 = dom ◡𝐵
8	6, 7	uneq12i 4122	. 2 ⊢ (ran 𝐴 ∪ ran 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
9	4, 5, 8	3eqtr4i 2798	1 ⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵)

Syntax hints:   = wceq 1563   ∪ cun 3905  ^◡ccnv 5651  dom cdm 5652  ran crn 5653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-cnv 5660  df-dm 5662  df-rn 5663

This theorem is referenced by:  imaundi  6138  imaundir  6139  imadifssran  6140  rnpropg  6213  fun  6730  foun  6829  fpr  7141  f1ounsn  7260  sbthlem6  9068  fodomr  9104  fodomfir  9275  brwdom2  9523  ordtval  23307  noextend  27788  noextendseq  27789  axlowdimlem13  29213  ex-rn  30700  padct  32975  ffsrn  32985  esplyind  33882  locfinref  34148  esumrnmpt2  34375  satfrnmapom  35733  ptrest  38130  rntrclfvOAI  43284  tfsconcatrn  43931  rclexi  44203  rtrclex  44205  rtrclexi  44209  cnvrcl0  44213  rntrcl  44216  dfrtrcl5  44217  dfrcl2  44262  rntrclfv  44320  rnresun  45756