Theorem rnun 6009

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 6006	. . . 4 ⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵)
2	1	dmeqi 5773	. . 3 ⊢ dom ◡(𝐴 ∪ 𝐵) = dom (◡𝐴 ∪ ◡𝐵)
3		dmun 5779	. . 3 ⊢ dom (◡𝐴 ∪ ◡𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
4	2, 3	eqtri 2765	. 2 ⊢ dom ◡(𝐴 ∪ 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
5		df-rn 5562	. 2 ⊢ ran (𝐴 ∪ 𝐵) = dom ◡(𝐴 ∪ 𝐵)
6		df-rn 5562	. . 3 ⊢ ran 𝐴 = dom ◡𝐴
7		df-rn 5562	. . 3 ⊢ ran 𝐵 = dom ◡𝐵
8	6, 7	uneq12i 4075	. 2 ⊢ (ran 𝐴 ∪ ran 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
9	4, 5, 8	3eqtr4i 2775	1 ⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵)

Syntax hints:   = wceq 1543   ∪ cun 3864  ^◡ccnv 5550  dom cdm 5551  ran crn 5552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-12 2175  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054  df-opab 5116  df-cnv 5559  df-dm 5561  df-rn 5562

This theorem is referenced by:  imaundi  6013  imaundir  6014  rnpropg  6085  fun  6581  foun  6679  fpr  6969  sbthlem6  8761  fodomr  8797  brwdom2  9189  ordtval  22086  axlowdimlem13  27045  ex-rn  28523  padct  30774  ffsrn  30784  locfinref  31505  esumrnmpt2  31748  satfrnmapom  33045  noextend  33606  noextendseq  33607  ptrest  35513  rntrclfvOAI  40216  rclexi  40899  rtrclex  40901  rtrclexi  40905  cnvrcl0  40909  rntrcl  40912  dfrtrcl5  40913  dfrcl2  40959  rntrclfv  41017  rnresun  42389