Theorem rnun 6089

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 6086	. . . 4 ⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵)
2	1	dmeqi 5842	. . 3 ⊢ dom ◡(𝐴 ∪ 𝐵) = dom (◡𝐴 ∪ ◡𝐵)
3		dmun 5848	. . 3 ⊢ dom (◡𝐴 ∪ ◡𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
4	2, 3	eqtri 2753	. 2 ⊢ dom ◡(𝐴 ∪ 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
5		df-rn 5625	. 2 ⊢ ran (𝐴 ∪ 𝐵) = dom ◡(𝐴 ∪ 𝐵)
6		df-rn 5625	. . 3 ⊢ ran 𝐴 = dom ◡𝐴
7		df-rn 5625	. . 3 ⊢ ran 𝐵 = dom ◡𝐵
8	6, 7	uneq12i 4114	. 2 ⊢ (ran 𝐴 ∪ ran 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
9	4, 5, 8	3eqtr4i 2763	1 ⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵)

Syntax hints:   = wceq 1541   ∪ cun 3898  ^◡ccnv 5613  dom cdm 5614  ran crn 5615

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 2112  ax-9 2120  ax-10 2143  ax-12 2179  ax-ext 2702

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 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-br 5090  df-opab 5152  df-cnv 5622  df-dm 5624  df-rn 5625

This theorem is referenced by:  imaundi  6093  imaundir  6094  imadifssran  6095  rnpropg  6166  fun  6681  foun  6777  fpr  7082  f1ounsn  7201  sbthlem6  9000  fodomr  9036  fodomfir  9207  brwdom2  9454  ordtval  23097  noextend  27598  noextendseq  27599  axlowdimlem13  28925  ex-rn  30410  padct  32691  ffsrn  32701  locfinref  33844  esumrnmpt2  34071  satfrnmapom  35382  ptrest  37638  rntrclfvOAI  42703  tfsconcatrn  43354  rclexi  43627  rtrclex  43629  rtrclexi  43633  cnvrcl0  43637  rntrcl  43640  dfrtrcl5  43641  dfrcl2  43686  rntrclfv  43744  rnresun  45196