Theorem rnun 6120

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 6117	. . . 4 ⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵)
2	1	dmeqi 5870	. . 3 ⊢ dom ◡(𝐴 ∪ 𝐵) = dom (◡𝐴 ∪ ◡𝐵)
3		dmun 5876	. . 3 ⊢ dom (◡𝐴 ∪ ◡𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
4	2, 3	eqtri 2753	. 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 4131	. 2 ⊢ (ran 𝐴 ∪ ran 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
9	4, 5, 8	3eqtr4i 2763	1 ⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵)

Syntax hints:   = wceq 1540   ∪ cun 3914  ^◡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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-br 5110  df-opab 5172  df-cnv 5648  df-dm 5650  df-rn 5651

This theorem is referenced by:  imaundi  6124  imaundir  6125  imadifssran  6126  rnpropg  6197  fun  6724  foun  6820  fpr  7128  f1ounsn  7249  sbthlem6  9061  fodomr  9097  fodomfir  9285  brwdom2  9532  ordtval  23082  noextend  27584  noextendseq  27585  axlowdimlem13  28887  ex-rn  30375  padct  32649  ffsrn  32658  locfinref  33837  esumrnmpt2  34064  satfrnmapom  35357  ptrest  37608  rntrclfvOAI  42672  tfsconcatrn  43324  rclexi  43597  rtrclex  43599  rtrclexi  43603  cnvrcl0  43607  rntrcl  43610  dfrtrcl5  43611  dfrcl2  43656  rntrclfv  43714  rnresun  45167