Theorem rnun 6110

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 6107	. . . 4 ⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵)
2	1	dmeqi 5860	. . 3 ⊢ dom ◡(𝐴 ∪ 𝐵) = dom (◡𝐴 ∪ ◡𝐵)
3		dmun 5866	. . 3 ⊢ dom (◡𝐴 ∪ ◡𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
4	2, 3	eqtri 2760	. 2 ⊢ dom ◡(𝐴 ∪ 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
5		df-rn 5642	. 2 ⊢ ran (𝐴 ∪ 𝐵) = dom ◡(𝐴 ∪ 𝐵)
6		df-rn 5642	. . 3 ⊢ ran 𝐴 = dom ◡𝐴
7		df-rn 5642	. . 3 ⊢ ran 𝐵 = dom ◡𝐵
8	6, 7	uneq12i 4107	. 2 ⊢ (ran 𝐴 ∪ ran 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
9	4, 5, 8	3eqtr4i 2770	1 ⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵)

Syntax hints:   = wceq 1542   ∪ cun 3888  ^◡ccnv 5630  dom cdm 5631  ran crn 5632

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  imaundi  6114  imaundir  6115  imadifssran  6116  rnpropg  6187  fun  6703  foun  6799  fpr  7108  f1ounsn  7227  sbthlem6  9030  fodomr  9066  fodomfir  9238  brwdom2  9488  ordtval  23154  noextend  27630  noextendseq  27631  axlowdimlem13  29023  ex-rn  30510  padct  32791  ffsrn  32801  esplyind  33719  locfinref  33985  esumrnmpt2  34212  satfrnmapom  35552  ptrest  37940  rntrclfvOAI  43123  tfsconcatrn  43770  rclexi  44042  rtrclex  44044  rtrclexi  44048  cnvrcl0  44052  rntrcl  44055  dfrtrcl5  44056  dfrcl2  44101  rntrclfv  44159  rnresun  45610