Theorem foima 6792

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

Step	Hyp	Ref	Expression
1		imadmrn 6055	. 2 ⊢ (𝐹 “ dom 𝐹) = ran 𝐹
2		fof 6787	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
3	2	fdmd 6713	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 → dom 𝐹 = 𝐴)
4	3	imaeq2d 6045	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ dom 𝐹) = (𝐹 “ 𝐴))
5		forn 6790	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
6	1, 4, 5	3eqtr3a 2793	1 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ 𝐴) = 𝐵)

Syntax hints:   → wi 4   = wceq 1539  dom cdm 5652  ran crn 5653   “ cima 5655  –onto→wfo 6526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5264  ax-nul 5274  ax-pr 5400

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-br 5118  df-opab 5180  df-xp 5658  df-cnv 5660  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-fn 6531  df-f 6532  df-fo 6534

This theorem is referenced by:  foimacnv  6832  fodomfi  9317  domunfican  9328  fiint  9333  fiintOLD  9334  fodomfiOLD  9337  cantnflt2  9680  cantnfp1lem3  9687  enfin1ai  10391  symgfixelsi  19403  dprdf1o  20002  lmimlbs  21783  cncmp  23317  cmpfi  23333  cnconn  23347  qtopval2  23621  elfm3  23875  rnelfm  23878  fmfnfmlem2  23880  fmfnfm  23883  eupthvdres  30150  pjordi  32088  qtophaus  33796  poimirlem1  37574  poimirlem2  37575  poimirlem3  37576  poimirlem4  37577  poimirlem5  37578  poimirlem6  37579  poimirlem7  37580  poimirlem9  37582  poimirlem10  37583  poimirlem11  37584  poimirlem12  37585  poimirlem14  37587  poimirlem16  37589  poimirlem17  37590  poimirlem19  37592  poimirlem20  37593  poimirlem22  37595  poimirlem23  37596  poimirlem24  37597  poimirlem25  37598  poimirlem29  37602  poimirlem31  37604  ovoliunnfl  37615  voliunnfl  37617  volsupnfl  37618  ismtybndlem  37759  riccrng1  42476  ricdrng1  42483  kelac1  43019  gicabl  43055  imasubc  48961