MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rnun Structured version   Visualization version   GIF version

Theorem rnun 6135
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
StepHypRef Expression
1 cnvun 6132 . . . 4 (𝐴𝐵) = (𝐴𝐵)
21dmeqi 5897 . . 3 dom (𝐴𝐵) = dom (𝐴𝐵)
3 dmun 5903 . . 3 dom (𝐴𝐵) = (dom 𝐴 ∪ dom 𝐵)
42, 3eqtri 2760 . 2 dom (𝐴𝐵) = (dom 𝐴 ∪ dom 𝐵)
5 df-rn 5681 . 2 ran (𝐴𝐵) = dom (𝐴𝐵)
6 df-rn 5681 . . 3 ran 𝐴 = dom 𝐴
7 df-rn 5681 . . 3 ran 𝐵 = dom 𝐵
86, 7uneq12i 4158 . 2 (ran 𝐴 ∪ ran 𝐵) = (dom 𝐴 ∪ dom 𝐵)
94, 5, 83eqtr4i 2770 1 ran (𝐴𝐵) = (ran 𝐴 ∪ ran 𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  cun 3943  ccnv 5669  dom cdm 5670  ran crn 5671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-br 5143  df-opab 5205  df-cnv 5678  df-dm 5680  df-rn 5681
This theorem is referenced by:  imaundi  6139  imaundir  6140  rnpropg  6211  fun  6741  foun  6839  fpr  7137  sbthlem6  9073  fodomr  9113  brwdom2  9552  ordtval  22624  noextend  27098  noextendseq  27099  axlowdimlem13  28141  ex-rn  29622  padct  31879  ffsrn  31889  locfinref  32716  esumrnmpt2  32961  satfrnmapom  34256  ptrest  36355  rntrclfvOAI  41264  tfsconcatrn  41927  rclexi  42201  rtrclex  42203  rtrclexi  42207  cnvrcl0  42211  rntrcl  42214  dfrtrcl5  42215  dfrcl2  42260  rntrclfv  42318  rnresun  43711
  Copyright terms: Public domain W3C validator