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

Theorem imaundi 6010
Description: Distributive law for image over union. Theorem 35 of [Suppes] p. 65. (Contributed by NM, 30-Sep-2002.)
Assertion
Ref Expression
imaundi (𝐴 “ (𝐵𝐶)) = ((𝐴𝐵) ∪ (𝐴𝐶))

Proof of Theorem imaundi
StepHypRef Expression
1 resundi 5869 . . . 4 (𝐴 ↾ (𝐵𝐶)) = ((𝐴𝐵) ∪ (𝐴𝐶))
21rneqi 5809 . . 3 ran (𝐴 ↾ (𝐵𝐶)) = ran ((𝐴𝐵) ∪ (𝐴𝐶))
3 rnun 6006 . . 3 ran ((𝐴𝐵) ∪ (𝐴𝐶)) = (ran (𝐴𝐵) ∪ ran (𝐴𝐶))
42, 3eqtri 2846 . 2 ran (𝐴 ↾ (𝐵𝐶)) = (ran (𝐴𝐵) ∪ ran (𝐴𝐶))
5 df-ima 5570 . 2 (𝐴 “ (𝐵𝐶)) = ran (𝐴 ↾ (𝐵𝐶))
6 df-ima 5570 . . 3 (𝐴𝐵) = ran (𝐴𝐵)
7 df-ima 5570 . . 3 (𝐴𝐶) = ran (𝐴𝐶)
86, 7uneq12i 4139 . 2 ((𝐴𝐵) ∪ (𝐴𝐶)) = (ran (𝐴𝐵) ∪ ran (𝐴𝐶))
94, 5, 83eqtr4i 2856 1 (𝐴 “ (𝐵𝐶)) = ((𝐴𝐵) ∪ (𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  cun 3936  ran crn 5558  cres 5559  cima 5560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-xp 5563  df-cnv 5565  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570
This theorem is referenced by:  fnimapr  6749  domunfican  8793  fiint  8797  fodomfi  8799  marypha1lem  8899  resunimafz0  13806  dprd2da  19166  dmdprdsplit2lem  19169  uniioombllem3  24188  mbfimaicc  24234  plyeq0  24803  fnimatp  30425  ffsrn  30467  tocyccntz  30788  noetalem4  33222  imadifss  34869  poimirlem1  34895  poimirlem2  34896  poimirlem3  34897  poimirlem4  34898  poimirlem6  34900  poimirlem7  34901  poimirlem11  34905  poimirlem12  34906  poimirlem15  34909  poimirlem16  34910  poimirlem17  34911  poimirlem19  34913  poimirlem20  34914  poimirlem23  34917  poimirlem24  34918  poimirlem25  34919  poimirlem29  34923  poimirlem31  34925  mbfposadd  34941  itg2addnclem2  34946  ftc1anclem1  34969  ftc1anclem5  34973  brtrclfv2  40079  frege77d  40098  frege109d  40109  frege131d  40116  dffrege76  40292  icccncfext  42177
  Copyright terms: Public domain W3C validator