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

Theorem rnun 6009
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 6006 . . . 4 (𝐴𝐵) = (𝐴𝐵)
21dmeqi 5773 . . 3 dom (𝐴𝐵) = dom (𝐴𝐵)
3 dmun 5779 . . 3 dom (𝐴𝐵) = (dom 𝐴 ∪ dom 𝐵)
42, 3eqtri 2765 . 2 dom (𝐴𝐵) = (dom 𝐴 ∪ dom 𝐵)
5 df-rn 5562 . 2 ran (𝐴𝐵) = dom (𝐴𝐵)
6 df-rn 5562 . . 3 ran 𝐴 = dom 𝐴
7 df-rn 5562 . . 3 ran 𝐵 = dom 𝐵
86, 7uneq12i 4075 . 2 (ran 𝐴 ∪ ran 𝐵) = (dom 𝐴 ∪ dom 𝐵)
94, 5, 83eqtr4i 2775 1 ran (𝐴𝐵) = (ran 𝐴 ∪ ran 𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1543  cun 3864  ccnv 5550  dom cdm 5551  ran crn 5552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-12 2175  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054  df-opab 5116  df-cnv 5559  df-dm 5561  df-rn 5562
This theorem is referenced by:  imaundi  6013  imaundir  6014  rnpropg  6085  fun  6581  foun  6679  fpr  6969  sbthlem6  8761  fodomr  8797  brwdom2  9189  ordtval  22086  axlowdimlem13  27045  ex-rn  28523  padct  30774  ffsrn  30784  locfinref  31505  esumrnmpt2  31748  satfrnmapom  33045  noextend  33606  noextendseq  33607  ptrest  35513  rntrclfvOAI  40216  rclexi  40899  rtrclex  40901  rtrclexi  40905  cnvrcl0  40909  rntrcl  40912  dfrtrcl5  40913  dfrcl2  40959  rntrclfv  41017  rnresun  42389
  Copyright terms: Public domain W3C validator