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

Theorem imain 6513
Description: The image of an intersection is the intersection of images. (Contributed by Paul Chapman, 11-Apr-2009.)
Assertion
Ref Expression
imain (Fun 𝐹 → (𝐹 “ (𝐴𝐵)) = ((𝐹𝐴) ∩ (𝐹𝐵)))

Proof of Theorem imain
StepHypRef Expression
1 imadif 6512 . . 3 (Fun 𝐹 → (𝐹 “ (𝐴 ∖ (𝐴𝐵))) = ((𝐹𝐴) ∖ (𝐹 “ (𝐴𝐵))))
2 imadif 6512 . . . 4 (Fun 𝐹 → (𝐹 “ (𝐴𝐵)) = ((𝐹𝐴) ∖ (𝐹𝐵)))
32difeq2d 4058 . . 3 (Fun 𝐹 → ((𝐹𝐴) ∖ (𝐹 “ (𝐴𝐵))) = ((𝐹𝐴) ∖ ((𝐹𝐴) ∖ (𝐹𝐵))))
41, 3eqtrd 2778 . 2 (Fun 𝐹 → (𝐹 “ (𝐴 ∖ (𝐴𝐵))) = ((𝐹𝐴) ∖ ((𝐹𝐴) ∖ (𝐹𝐵))))
5 dfin4 4203 . . 3 (𝐴𝐵) = (𝐴 ∖ (𝐴𝐵))
65imaeq2i 5962 . 2 (𝐹 “ (𝐴𝐵)) = (𝐹 “ (𝐴 ∖ (𝐴𝐵)))
7 dfin4 4203 . 2 ((𝐹𝐴) ∩ (𝐹𝐵)) = ((𝐹𝐴) ∖ ((𝐹𝐴) ∖ (𝐹𝐵)))
84, 6, 73eqtr4g 2803 1 (Fun 𝐹 → (𝐹 “ (𝐴𝐵)) = ((𝐹𝐴) ∩ (𝐹𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539  cdif 3885  cin 3887  ccnv 5585  cima 5589  Fun wfun 6422
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3433  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-sn 4564  df-pr 4566  df-op 4570  df-br 5076  df-opab 5138  df-id 5486  df-xp 5592  df-rel 5593  df-cnv 5594  df-co 5595  df-dm 5596  df-rn 5597  df-res 5598  df-ima 5599  df-fun 6430
This theorem is referenced by:  inpreima  6935  rnelfmlem  23092  fmfnfmlem3  23096  spthispth  28081  swrdrndisj  31216  ballotlemfrc  32480  poimirlem1  35765  poimirlem2  35766  poimirlem3  35767  poimirlem4  35768  poimirlem6  35770  poimirlem7  35771  poimirlem11  35775  poimirlem12  35776  poimirlem16  35780  poimirlem17  35781  poimirlem19  35783  poimirlem20  35784  poimirlem23  35787  poimirlem24  35788  poimirlem25  35789  poimirlem29  35793  poimirlem31  35795
  Copyright terms: Public domain W3C validator