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

Theorem imaundi 5408
Description: Distributive law for image over union. Theorem 35 of [Suppes] p. 65. (Contributed by NM, 30-Sep-2002.)
Assertion
Ref Expression
imaundi  |-  ( A
" ( B  u.  C ) )  =  ( ( A " B )  u.  ( A " C ) )

Proof of Theorem imaundi
StepHypRef Expression
1 resundi 5277 . . . 4  |-  ( A  |`  ( B  u.  C
) )  =  ( ( A  |`  B )  u.  ( A  |`  C ) )
21rneqi 5219 . . 3  |-  ran  ( A  |`  ( B  u.  C ) )  =  ran  ( ( A  |`  B )  u.  ( A  |`  C ) )
3 rnun 5404 . . 3  |-  ran  (
( A  |`  B )  u.  ( A  |`  C ) )  =  ( ran  ( A  |`  B )  u.  ran  ( A  |`  C ) )
42, 3eqtri 2472 . 2  |-  ran  ( A  |`  ( B  u.  C ) )  =  ( ran  ( A  |`  B )  u.  ran  ( A  |`  C ) )
5 df-ima 5002 . 2  |-  ( A
" ( B  u.  C ) )  =  ran  ( A  |`  ( B  u.  C
) )
6 df-ima 5002 . . 3  |-  ( A
" B )  =  ran  ( A  |`  B )
7 df-ima 5002 . . 3  |-  ( A
" C )  =  ran  ( A  |`  C )
86, 7uneq12i 3641 . 2  |-  ( ( A " B )  u.  ( A " C ) )  =  ( ran  ( A  |`  B )  u.  ran  ( A  |`  C ) )
94, 5, 83eqtr4i 2482 1  |-  ( A
" ( B  u.  C ) )  =  ( ( A " B )  u.  ( A " C ) )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1383    u. cun 3459   ran crn 4990    |` cres 4991   "cima 4992
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438  df-opab 4496  df-xp 4995  df-cnv 4997  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002
This theorem is referenced by:  fnimapr  5922  domunfican  7795  fiint  7799  fodomfi  7801  marypha1lem  7895  dprd2da  17070  dmdprdsplit2lem  17073  uniioombllem3  21972  mbfimaicc  22018  plyeq0  22586  eupath2lem3  24957  ffsrn  27530  mbfposadd  30038  itg2addnclem2  30043  ftc1anclem1  30066  ftc1anclem5  30070  icccncfext  31644
  Copyright terms: Public domain W3C validator