Theorem rnun 6142

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 6139	. . . 4 ⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵)
2	1	dmeqi 5894	. . 3 ⊢ dom ◡(𝐴 ∪ 𝐵) = dom (◡𝐴 ∪ ◡𝐵)
3		dmun 5900	. . 3 ⊢ dom (◡𝐴 ∪ ◡𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
4	2, 3	eqtri 2784	. 2 ⊢ dom ◡(𝐴 ∪ 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
5		df-rn 5672	. 2 ⊢ ran (𝐴 ∪ 𝐵) = dom ◡(𝐴 ∪ 𝐵)
6		df-rn 5672	. . 3 ⊢ ran 𝐴 = dom ◡𝐴
7		df-rn 5672	. . 3 ⊢ ran 𝐵 = dom ◡𝐵
8	6, 7	uneq12i 4119	. 2 ⊢ (ran 𝐴 ∪ ran 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
9	4, 5, 8	3eqtr4i 2794	1 ⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵)

Syntax hints:   = wceq 1568   ∪ cun 3902  ^◡ccnv 5660  dom cdm 5661  ran crn 5662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-opab 5173  df-cnv 5669  df-dm 5671  df-rn 5672

This theorem is referenced by:  imaundi  6147  imaundir  6148  imadifssran  6202  imadifssranOLD  6203  rnpropg  6223  fun  6740  foun  6839  fpr  7151  f1ounsn  7270  sbthlem6  9079  fodomr  9115  fodomfir  9286  brwdom2  9534  ordtval  23325  noextend  27806  noextendseq  27807  axlowdimlem13  29270  ex-rn  30757  padct  33029  ffsrn  33039  esplyind  33931  locfinref  34197  esumrnmpt2  34424  satfrnmapom  35828  ptrest  38236  rntrclfvOAI  43392  tfsconcatrn  44039  rclexi  44311  rtrclex  44313  rtrclexi  44317  cnvrcl0  44321  rntrcl  44324  dfrtrcl5  44325  dfrcl2  44370  rntrclfv  44428  rnresun  45868