Theorem foima 6801

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 6074	. 2 ⊢ (𝐹 “ dom 𝐹) = ran 𝐹
2		fof 6796	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
3	2	fdmd 6720	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 → dom 𝐹 = 𝐴)
4	3	imaeq2d 6064	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ dom 𝐹) = (𝐹 “ 𝐴))
5		forn 6799	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
6	1, 4, 5	3eqtr3a 2824	1 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ 𝐴) = 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5663  ran crn 5664   “ cima 5666  –onto→wfo 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-xp 5669  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-fn 6543  df-f 6544  df-fo 6546

This theorem is used by:  foimacnv  6842  fodomfi  9275  domunfican  9284  fiint  9289  cantnflt2  9645  cantnfp1lem3  9652  enfin1ai  10379  symgfixelsi  19528  dprdf1o  20127  lmimlbs  22015  cncmp  23578  cmpfi  23594  cnconn  23608  qtopval2  23882  elfm3  24136  rnelfm  24139  fmfnfmlem2  24141  fmfnfm  24144  eupthvdres  30615  pjordi  32554  qtophaus  34249  poimirlem1  38305  poimirlem2  38306  poimirlem3  38307  poimirlem4  38308  poimirlem5  38309  poimirlem6  38310  poimirlem7  38311  poimirlem9  38313  poimirlem10  38314  poimirlem11  38315  poimirlem12  38316  poimirlem14  38318  poimirlem16  38320  poimirlem17  38321  poimirlem19  38323  poimirlem20  38324  poimirlem22  38326  poimirlem23  38327  poimirlem24  38328  poimirlem25  38329  poimirlem29  38333  poimirlem31  38335  ovoliunnfl  38346  voliunnfl  38348  volsupnfl  38349  ismtybndlem  38490  riccrng1  43322  ricdrng1  43329  kelac1  43823  gicabl  43859  imasubc  49962