Theorem rnun 6119

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 6116	. . . 4 ⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵)
2	1	dmeqi 5873	. . 3 ⊢ dom ◡(𝐴 ∪ 𝐵) = dom (◡𝐴 ∪ ◡𝐵)
3		dmun 5879	. . 3 ⊢ dom (◡𝐴 ∪ ◡𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
4	2, 3	eqtri 2779	. 2 ⊢ dom ◡(𝐴 ∪ 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
5		df-rn 5651	. 2 ⊢ ran (𝐴 ∪ 𝐵) = dom ◡(𝐴 ∪ 𝐵)
6		df-rn 5651	. . 3 ⊢ ran 𝐴 = dom ◡𝐴
7		df-rn 5651	. . 3 ⊢ ran 𝐵 = dom ◡𝐵
8	6, 7	uneq12i 4114	. 2 ⊢ (ran 𝐴 ∪ ran 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
9	4, 5, 8	3eqtr4i 2789	1 ⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵)

Syntax hints:   = wceq 1554   ∪ cun 3897  ^◡ccnv 5639  dom cdm 5640  ran crn 5641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-br 5095  df-opab 5157  df-cnv 5648  df-dm 5650  df-rn 5651

This theorem is referenced by:  imaundi  6124  imaundir  6125  imadifssran  6126  rnpropg  6198  fun  6715  foun  6814  fpr  7126  f1ounsn  7245  sbthlem6  9053  fodomr  9089  fodomfir  9261  brwdom2  9511  ordtval  23222  noextend  27700  noextendseq  27701  axlowdimlem13  29094  ex-rn  30581  padct  32863  ffsrn  32873  esplyind  33826  locfinref  34092  esumrnmpt2  34319  satfrnmapom  35668  ptrest  38066  rntrclfvOAI  43220  tfsconcatrn  43867  rclexi  44139  rtrclex  44141  rtrclexi  44145  cnvrcl0  44149  rntrcl  44152  dfrtrcl5  44153  dfrcl2  44198  rntrclfv  44256  rnresun  45706