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

Theorem imaundir 5985
Description: The image of a union. (Contributed by Jeff Hoffman, 17-Feb-2008.)
Assertion
Ref Expression
imaundir ((𝐴𝐵) “ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))

Proof of Theorem imaundir
StepHypRef Expression
1 df-ima 5544 . . 3 ((𝐴𝐵) “ 𝐶) = ran ((𝐴𝐵) ↾ 𝐶)
2 resundir 5844 . . . 4 ((𝐴𝐵) ↾ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))
32rneqi 5783 . . 3 ran ((𝐴𝐵) ↾ 𝐶) = ran ((𝐴𝐶) ∪ (𝐵𝐶))
4 rnun 5980 . . 3 ran ((𝐴𝐶) ∪ (𝐵𝐶)) = (ran (𝐴𝐶) ∪ ran (𝐵𝐶))
51, 3, 43eqtri 2847 . 2 ((𝐴𝐵) “ 𝐶) = (ran (𝐴𝐶) ∪ ran (𝐵𝐶))
6 df-ima 5544 . . 3 (𝐴𝐶) = ran (𝐴𝐶)
7 df-ima 5544 . . 3 (𝐵𝐶) = ran (𝐵𝐶)
86, 7uneq12i 4116 . 2 ((𝐴𝐶) ∪ (𝐵𝐶)) = (ran (𝐴𝐶) ∪ ran (𝐵𝐶))
95, 8eqtr4i 2846 1 ((𝐴𝐵) “ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  cun 3911  ran crn 5532  cres 5533  cima 5534
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 2792
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 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-rab 3134  df-v 3475  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-sn 4544  df-pr 4546  df-op 4550  df-br 5043  df-opab 5105  df-cnv 5539  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544
This theorem is referenced by:  fvun  6729  suppun  7828  fsuppun  8830  fpwwe2lem13  10042  ustuqtop1  22826  mbfres2  24228  imadifxp  30338  eulerpartlemt  31637  bj-projun  34323  bj-funun  34551  poimirlem3  34936  poimirlem15  34948  brtrclfv2  40207  frege131d  40244  unhe1  40266  frege110  40454  frege133  40477  aacllem  45089
  Copyright terms: Public domain W3C validator