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

Theorem rnun 6146
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 6143 . . . 4 (𝐴𝐵) = (𝐴𝐵)
21dmeqi 5905 . . 3 dom (𝐴𝐵) = dom (𝐴𝐵)
3 dmun 5911 . . 3 dom (𝐴𝐵) = (dom 𝐴 ∪ dom 𝐵)
42, 3eqtri 2761 . 2 dom (𝐴𝐵) = (dom 𝐴 ∪ dom 𝐵)
5 df-rn 5688 . 2 ran (𝐴𝐵) = dom (𝐴𝐵)
6 df-rn 5688 . . 3 ran 𝐴 = dom 𝐴
7 df-rn 5688 . . 3 ran 𝐵 = dom 𝐵
86, 7uneq12i 4162 . 2 (ran 𝐴 ∪ ran 𝐵) = (dom 𝐴 ∪ dom 𝐵)
94, 5, 83eqtr4i 2771 1 ran (𝐴𝐵) = (ran 𝐴 ∪ ran 𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  cun 3947  ccnv 5676  dom cdm 5677  ran crn 5678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-cnv 5685  df-dm 5687  df-rn 5688
This theorem is referenced by:  imaundi  6150  imaundir  6151  rnpropg  6222  fun  6754  foun  6852  fpr  7152  sbthlem6  9088  fodomr  9128  brwdom2  9568  ordtval  22693  noextend  27169  noextendseq  27170  axlowdimlem13  28212  ex-rn  29693  padct  31944  ffsrn  31954  locfinref  32821  esumrnmpt2  33066  satfrnmapom  34361  ptrest  36487  rntrclfvOAI  41429  tfsconcatrn  42092  rclexi  42366  rtrclex  42368  rtrclexi  42372  cnvrcl0  42376  rntrcl  42379  dfrtrcl5  42380  dfrcl2  42425  rntrclfv  42483  rnresun  43876
  Copyright terms: Public domain W3C validator