Theorem rnun 6135

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 6132	. . . 4 ⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵)
2	1	dmeqi 5897	. . 3 ⊢ dom ◡(𝐴 ∪ 𝐵) = dom (◡𝐴 ∪ ◡𝐵)
3		dmun 5903	. . 3 ⊢ dom (◡𝐴 ∪ ◡𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
4	2, 3	eqtri 2760	. 2 ⊢ dom ◡(𝐴 ∪ 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
5		df-rn 5681	. 2 ⊢ ran (𝐴 ∪ 𝐵) = dom ◡(𝐴 ∪ 𝐵)
6		df-rn 5681	. . 3 ⊢ ran 𝐴 = dom ◡𝐴
7		df-rn 5681	. . 3 ⊢ ran 𝐵 = dom ◡𝐵
8	6, 7	uneq12i 4158	. 2 ⊢ (ran 𝐴 ∪ ran 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
9	4, 5, 8	3eqtr4i 2770	1 ⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵)

Syntax hints:   = wceq 1541   ∪ cun 3943  ^◡ccnv 5669  dom cdm 5670  ran crn 5671

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-br 5143  df-opab 5205  df-cnv 5678  df-dm 5680  df-rn 5681

This theorem is referenced by:  imaundi  6139  imaundir  6140  rnpropg  6211  fun  6741  foun  6839  fpr  7137  sbthlem6  9073  fodomr  9113  brwdom2  9552  ordtval  22624  noextend  27098  noextendseq  27099  axlowdimlem13  28141  ex-rn  29622  padct  31879  ffsrn  31889  locfinref  32716  esumrnmpt2  32961  satfrnmapom  34256  ptrest  36355  rntrclfvOAI  41264  tfsconcatrn  41927  rclexi  42201  rtrclex  42203  rtrclexi  42207  cnvrcl0  42211  rntrcl  42214  dfrtrcl5  42215  dfrcl2  42260  rntrclfv  42318  rnresun  43711