Theorem rnun 6130

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 6127	. . . 4 ⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵)
2	1	dmeqi 5882	. . 3 ⊢ dom ◡(𝐴 ∪ 𝐵) = dom (◡𝐴 ∪ ◡𝐵)
3		dmun 5888	. . 3 ⊢ dom (◡𝐴 ∪ ◡𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
4	2, 3	eqtri 2783	. 2 ⊢ dom ◡(𝐴 ∪ 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
5		df-rn 5658	. 2 ⊢ ran (𝐴 ∪ 𝐵) = dom ◡(𝐴 ∪ 𝐵)
6		df-rn 5658	. . 3 ⊢ ran 𝐴 = dom ◡𝐴
7		df-rn 5658	. . 3 ⊢ ran 𝐵 = dom ◡𝐵
8	6, 7	uneq12i 4112	. 2 ⊢ (ran 𝐴 ∪ ran 𝐵) = (dom ◡𝐴 ∪ dom ◡𝐵)
9	4, 5, 8	3eqtr4i 2793	1 ⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵)

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 3896  ^◡ccnv 5646  dom cdm 5647  ran crn 5648

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-cnv 5655  df-dm 5657  df-rn 5658

This theorem is used by:  imaundi  6135  imaundir  6136  imadifssran  6191  imadifssranOLD  6192  rnpropg  6212  fun  6732  foun  6831  fpr  7146  f1ounsn  7268  sbthlem6  9089  fodomr  9125  fodomfir  9297  brwdom2  9545  ordtval  23469  noextend  27957  noextendseq  27958  axlowdimlem13  29466  ex-rn  30975  padct  33244  ffsrn  33254  esplyind  34141  locfinref  34407  esumrnmpt2  34634  satfrnmapom  36056  ptrest  38457  rntrclfvOAI  43640  tfsconcatrn  44287  rclexi  44559  rtrclex  44561  rtrclexi  44565  cnvrcl0  44569  rntrcl  44572  dfrtrcl5  44573  dfrcl2  44618  rntrclfv  44676  rnresun  46116