Theorem rnun 6141

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 6138	. . . 4 ⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵)
2	1	dmeqi 5893	. . 3 ⊢ dom ◡(𝐴 ∪ 𝐵) = dom (◡𝐴 ∪ ◡𝐵)
3		dmun 5899	. . 3 ⊢ dom (◡𝐴 ∪ ◡𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
4	2, 3	eqtri 2785	. 2 ⊢ dom ◡(𝐴 ∪ 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
5		df-rn 5671	. 2 ⊢ ran (𝐴 ∪ 𝐵) = dom ◡(𝐴 ∪ 𝐵)
6		df-rn 5671	. . 3 ⊢ ran 𝐴 = dom ◡𝐴
7		df-rn 5671	. . 3 ⊢ ran 𝐵 = dom ◡𝐵
8	6, 7	uneq12i 4119	. 2 ⊢ (ran 𝐴 ∪ ran 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
9	4, 5, 8	3eqtr4i 2795	1 ⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵)

This proof depends on syntax axioms:   = wceq 1569   ∪ cun 3902  ^◡ccnv 5659  dom cdm 5660  ran crn 5661

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  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 5668  df-dm 5670  df-rn 5671

This theorem is used by:  imaundi  6146  imaundir  6147  imadifssran  6201  imadifssranOLD  6202  rnpropg  6222  fun  6740  foun  6839  fpr  7151  f1ounsn  7270  sbthlem6  9078  fodomr  9114  fodomfir  9285  brwdom2  9533  ordtval  23357  noextend  27841  noextendseq  27842  axlowdimlem13  29315  ex-rn  30802  padct  33074  ffsrn  33084  esplyind  33974  locfinref  34240  esumrnmpt2  34467  satfrnmapom  35870  ptrest  38298  rntrclfvOAI  43450  tfsconcatrn  44097  rclexi  44369  rtrclex  44371  rtrclexi  44375  cnvrcl0  44379  rntrcl  44382  dfrtrcl5  44383  dfrcl2  44428  rntrclfv  44486  rnresun  45926