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

Theorem foima 6762
Description: The image of the domain of an onto function. (Contributed by NM, 29-Nov-2002.)
Assertion
Ref Expression
foima (𝐹:𝐴onto𝐵 → (𝐹𝐴) = 𝐵)

Proof of Theorem foima
StepHypRef Expression
1 imadmrn 6024 . 2 (𝐹 “ dom 𝐹) = ran 𝐹
2 fof 6757 . . . 4 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
32fdmd 6680 . . 3 (𝐹:𝐴onto𝐵 → dom 𝐹 = 𝐴)
43imaeq2d 6014 . 2 (𝐹:𝐴onto𝐵 → (𝐹 “ dom 𝐹) = (𝐹𝐴))
5 forn 6760 . 2 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
61, 4, 53eqtr3a 2801 1 (𝐹:𝐴onto𝐵 → (𝐹𝐴) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  dom cdm 5634  ran crn 5635  cima 5637  ontowfo 6495
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-xp 5640  df-cnv 5642  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-fn 6500  df-f 6501  df-fo 6503
This theorem is referenced by:  foimacnv  6802  domunfican  9265  fiint  9269  fodomfi  9270  cantnflt2  9610  cantnfp1lem3  9617  enfin1ai  10321  symgfixelsi  19218  dprdf1o  19812  lmimlbs  21245  cncmp  22746  cmpfi  22762  cnconn  22776  qtopval2  23050  elfm3  23304  rnelfm  23307  fmfnfmlem2  23309  fmfnfm  23312  eupthvdres  29182  pjordi  31118  qtophaus  32420  poimirlem1  36082  poimirlem2  36083  poimirlem3  36084  poimirlem4  36085  poimirlem5  36086  poimirlem6  36087  poimirlem7  36088  poimirlem9  36090  poimirlem10  36091  poimirlem11  36092  poimirlem12  36093  poimirlem14  36095  poimirlem16  36097  poimirlem17  36098  poimirlem19  36100  poimirlem20  36101  poimirlem22  36103  poimirlem23  36104  poimirlem24  36105  poimirlem25  36106  poimirlem29  36110  poimirlem31  36112  ovoliunnfl  36123  voliunnfl  36125  volsupnfl  36126  ismtybndlem  36268  riccrng1  40706  ricdrng1  40720  kelac1  41393  gicabl  41429
  Copyright terms: Public domain W3C validator