Theorem rnun 6148

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 6145	. . . 4 ⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵)
2	1	dmeqi 5893	. . 3 ⊢ dom ◡(𝐴 ∪ 𝐵) = dom (◡𝐴 ∪ ◡𝐵)
3		dmun 5899	. . 3 ⊢ dom (◡𝐴 ∪ ◡𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
4	2, 3	eqtri 2786	. 2 ⊢ dom ◡(𝐴 ∪ 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
5		df-rn 5666	. 2 ⊢ ran (𝐴 ∪ 𝐵) = dom ◡(𝐴 ∪ 𝐵)
6		df-rn 5666	. . 3 ⊢ ran 𝐴 = dom ◡𝐴
7		df-rn 5666	. . 3 ⊢ ran 𝐵 = dom ◡𝐵
8	6, 7	uneq12i 4168	. 2 ⊢ (ran 𝐴 ∪ ran 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
9	4, 5, 8	3eqtr4i 2796	1 ⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵)

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 4152  ^◡ccnv 5654  dom cdm 5655  ran crn 5656

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-cnv 5663  df-dm 5665  df-rn 5666

This theorem is used by:  imaundi  6153  imaundir  6154  imadifssranOLD  6215  imadifssranOLDOLD  6216  rnpropg  6236  fun  6766  foun  6865  fpr  7182  f1ounsn  7303  sbthlem6  9139  fodomr  9175  fodomfir  9347  brwdom2  9594  ordtval  23537  noextend  28053  noextendseq  28054  axlowdimlem13  29562  ex-rn  31071  padct  33381  ffsrn  33390  esplyind  34277  locfinref  34543  esumrnmpt2  34770  satfrnmapom  36302  ptrest  38729  rntrclfvOAI  43895  tfsconcatrn  44536  rclexi  44807  rtrclex  44809  rtrclexi  44813  cnvrcl0  44817  rntrcl  44820  dfrtrcl5  44821  dfrcl2  44866  rntrclfv  44924  rnresun  46400