Theorem rnun 6098

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 6095	. . . 4 ⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵)
2	1	dmeqi 5849	. . 3 ⊢ dom ◡(𝐴 ∪ 𝐵) = dom (◡𝐴 ∪ ◡𝐵)
3		dmun 5855	. . 3 ⊢ dom (◡𝐴 ∪ ◡𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
4	2, 3	eqtri 2754	. 2 ⊢ dom ◡(𝐴 ∪ 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
5		df-rn 5630	. 2 ⊢ ran (𝐴 ∪ 𝐵) = dom ◡(𝐴 ∪ 𝐵)
6		df-rn 5630	. . 3 ⊢ ran 𝐴 = dom ◡𝐴
7		df-rn 5630	. . 3 ⊢ ran 𝐵 = dom ◡𝐵
8	6, 7	uneq12i 4115	. 2 ⊢ (ran 𝐴 ∪ ran 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
9	4, 5, 8	3eqtr4i 2764	1 ⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵)

Syntax hints:   = wceq 1541   ∪ cun 3895  ^◡ccnv 5618  dom cdm 5619  ran crn 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-cnv 5627  df-dm 5629  df-rn 5630

This theorem is referenced by:  imaundi  6102  imaundir  6103  imadifssran  6104  rnpropg  6175  fun  6691  foun  6787  fpr  7093  f1ounsn  7212  sbthlem6  9011  fodomr  9047  fodomfir  9218  brwdom2  9465  ordtval  23110  noextend  27611  noextendseq  27612  axlowdimlem13  28939  ex-rn  30427  padct  32708  ffsrn  32718  locfinref  33861  esumrnmpt2  34088  satfrnmapom  35421  ptrest  37665  rntrclfvOAI  42789  tfsconcatrn  43440  rclexi  43713  rtrclex  43715  rtrclexi  43719  cnvrcl0  43723  rntrcl  43726  dfrtrcl5  43727  dfrcl2  43772  rntrclfv  43830  rnresun  45282