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

Theorem rnun 5250
Description: Distributive law for range over union. Theorem 8 of [Suppes] p. 60. (Contributed by NM, 24-Mar-1998.)
Assertion
Ref Expression
rnun  |-  ran  ( A  u.  B )  =  ( ran  A  u.  ran  B )

Proof of Theorem rnun
StepHypRef Expression
1 cnvun 5247 . . . 4  |-  `' ( A  u.  B )  =  ( `' A  u.  `' B )
21dmeqi 5041 . . 3  |-  dom  `' ( A  u.  B
)  =  dom  ( `' A  u.  `' B )
3 dmun 5047 . . 3  |-  dom  ( `' A  u.  `' B )  =  ( dom  `' A  u.  dom  `' B )
42, 3eqtri 2493 . 2  |-  dom  `' ( A  u.  B
)  =  ( dom  `' A  u.  dom  `' B )
5 df-rn 4850 . 2  |-  ran  ( A  u.  B )  =  dom  `' ( A  u.  B )
6 df-rn 4850 . . 3  |-  ran  A  =  dom  `' A
7 df-rn 4850 . . 3  |-  ran  B  =  dom  `' B
86, 7uneq12i 3577 . 2  |-  ( ran 
A  u.  ran  B
)  =  ( dom  `' A  u.  dom  `' B )
94, 5, 83eqtr4i 2503 1  |-  ran  ( A  u.  B )  =  ( ran  A  u.  ran  B )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1452    u. cun 3388   `'ccnv 4838   dom cdm 4839   ran crn 4840
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-br 4396  df-opab 4455  df-cnv 4847  df-dm 4849  df-rn 4850
This theorem is referenced by:  imaundi  5254  imaundir  5255  rnpropg  5323  fun  5758  foun  5846  fpr  6088  sbthlem6  7705  fodomr  7741  brwdom2  8106  ordtval  20282  axlowdimlem13  25063  ex-rn  25969  padct  28382  ffsrn  28389  locfinref  28742  esumrnmpt2  28963  ptrest  32003  rntrclfvOAI  35604  rclexi  36293  rtrclex  36295  rtrclexi  36299  cnvrcl0  36303  rntrcl  36306  dfrtrcl5  36307  dfrcl2  36337  rntrclfv  36395  rnresun  37519
  Copyright terms: Public domain W3C validator