Theorem rnun 6140

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 6137	. . . 4 ⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵)
2	1	dmeqi 5892	. . 3 ⊢ dom ◡(𝐴 ∪ 𝐵) = dom (◡𝐴 ∪ ◡𝐵)
3		dmun 5898	. . 3 ⊢ dom (◡𝐴 ∪ ◡𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
4	2, 3	eqtri 2785	. 2 ⊢ dom ◡(𝐴 ∪ 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
5		df-rn 5670	. 2 ⊢ ran (𝐴 ∪ 𝐵) = dom ◡(𝐴 ∪ 𝐵)
6		df-rn 5670	. . 3 ⊢ ran 𝐴 = dom ◡𝐴
7		df-rn 5670	. . 3 ⊢ ran 𝐵 = dom ◡𝐵
8	6, 7	uneq12i 4116	. 2 ⊢ (ran 𝐴 ∪ ran 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
9	4, 5, 8	3eqtr4i 2795	1 ⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵)

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 3900  ^◡ccnv 5658  dom cdm 5659  ran crn 5660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-cnv 5667  df-dm 5669  df-rn 5670

This theorem is used by:  imaundi  6145  imaundir  6146  imadifssran  6201  imadifssranOLD  6202  rnpropg  6222  fun  6741  foun  6840  fpr  7154  f1ounsn  7276  sbthlem6  9093  fodomr  9129  fodomfir  9300  brwdom2  9548  ordtval  23418  noextend  27903  noextendseq  27904  axlowdimlem13  29412  ex-rn  30921  padct  33191  ffsrn  33201  esplyind  34087  locfinref  34353  esumrnmpt2  34580  satfrnmapom  35951  ptrest  38370  rntrclfvOAI  43538  tfsconcatrn  44185  rclexi  44457  rtrclex  44459  rtrclexi  44463  cnvrcl0  44467  rntrcl  44470  dfrtrcl5  44471  dfrcl2  44516  rntrclfv  44574  rnresun  46014