Theorem foima 6751

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 6029	. 2 ⊢ (𝐹 “ dom 𝐹) = ran 𝐹
2		fof 6746	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
3	2	fdmd 6672	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 → dom 𝐹 = 𝐴)
4	3	imaeq2d 6019	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ dom 𝐹) = (𝐹 “ 𝐴))
5		forn 6749	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
6	1, 4, 5	3eqtr3a 2795	1 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ 𝐴) = 𝐵)

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5624  ran crn 5625   “ cima 5627  –onto→wfo 6490

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-fn 6495  df-f 6496  df-fo 6498

This theorem is referenced by:  foimacnv  6791  fodomfi  9212  domunfican  9222  fiint  9227  fodomfiOLD  9230  cantnflt2  9582  cantnfp1lem3  9589  enfin1ai  10294  symgfixelsi  19364  dprdf1o  19963  lmimlbs  21791  cncmp  23336  cmpfi  23352  cnconn  23366  qtopval2  23640  elfm3  23894  rnelfm  23897  fmfnfmlem2  23899  fmfnfm  23902  eupthvdres  30310  pjordi  32248  qtophaus  33993  poimirlem1  37822  poimirlem2  37823  poimirlem3  37824  poimirlem4  37825  poimirlem5  37826  poimirlem6  37827  poimirlem7  37828  poimirlem9  37830  poimirlem10  37831  poimirlem11  37832  poimirlem12  37833  poimirlem14  37835  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem22  37843  poimirlem23  37844  poimirlem24  37845  poimirlem25  37846  poimirlem29  37850  poimirlem31  37852  ovoliunnfl  37863  voliunnfl  37865  volsupnfl  37866  ismtybndlem  38007  riccrng1  42776  ricdrng1  42783  kelac1  43305  gicabl  43341  imasubc  49396