Theorem rnun 6103

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 6100	. . . 4 ⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵)
2	1	dmeqi 5853	. . 3 ⊢ dom ◡(𝐴 ∪ 𝐵) = dom (◡𝐴 ∪ ◡𝐵)
3		dmun 5859	. . 3 ⊢ dom (◡𝐴 ∪ ◡𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
4	2, 3	eqtri 2763	. 2 ⊢ dom ◡(𝐴 ∪ 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
5		df-rn 5636	. 2 ⊢ ran (𝐴 ∪ 𝐵) = dom ◡(𝐴 ∪ 𝐵)
6		df-rn 5636	. . 3 ⊢ ran 𝐴 = dom ◡𝐴
7		df-rn 5636	. . 3 ⊢ ran 𝐵 = dom ◡𝐵
8	6, 7	uneq12i 4103	. 2 ⊢ (ran 𝐴 ∪ ran 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
9	4, 5, 8	3eqtr4i 2773	1 ⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵)

Syntax hints:   = wceq 1547   ∪ cun 3888  ^◡ccnv 5624  dom cdm 5625  ran crn 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-cnv 5633  df-dm 5635  df-rn 5636

This theorem is referenced by:  imaundi  6107  imaundir  6108  imadifssran  6109  rnpropg  6180  fun  6696  foun  6792  fpr  7104  f1ounsn  7223  sbthlem6  9027  fodomr  9063  fodomfir  9235  brwdom2  9485  ordtval  23179  noextend  27655  noextendseq  27656  axlowdimlem13  29048  ex-rn  30535  padct  32817  ffsrn  32827  esplyind  33766  locfinref  34032  esumrnmpt2  34259  satfrnmapom  35599  ptrest  37987  rntrclfvOAI  43141  tfsconcatrn  43788  rclexi  44060  rtrclex  44062  rtrclexi  44066  cnvrcl0  44070  rntrcl  44073  dfrtrcl5  44074  dfrcl2  44119  rntrclfv  44177  rnresun  45628