Theorem foima 6735

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 6014	. 2 ⊢ (𝐹 “ dom 𝐹) = ran 𝐹
2		fof 6730	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
3	2	fdmd 6656	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 → dom 𝐹 = 𝐴)
4	3	imaeq2d 6004	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ dom 𝐹) = (𝐹 “ 𝐴))
5		forn 6733	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
6	1, 4, 5	3eqtr3a 2790	1 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ 𝐴) = 𝐵)

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5611  ran crn 5612   “ cima 5614  –onto→wfo 6474

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365

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 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-br 5087  df-opab 5149  df-xp 5617  df-cnv 5619  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-fn 6479  df-f 6480  df-fo 6482

This theorem is referenced by:  foimacnv  6775  fodomfi  9191  domunfican  9201  fiint  9206  fodomfiOLD  9209  cantnflt2  9558  cantnfp1lem3  9565  enfin1ai  10270  symgfixelsi  19342  dprdf1o  19941  lmimlbs  21768  cncmp  23302  cmpfi  23318  cnconn  23332  qtopval2  23606  elfm3  23860  rnelfm  23863  fmfnfmlem2  23865  fmfnfm  23868  eupthvdres  30207  pjordi  32145  qtophaus  33841  poimirlem1  37661  poimirlem2  37662  poimirlem3  37663  poimirlem4  37664  poimirlem5  37665  poimirlem6  37666  poimirlem7  37667  poimirlem9  37669  poimirlem10  37670  poimirlem11  37671  poimirlem12  37672  poimirlem14  37674  poimirlem16  37676  poimirlem17  37677  poimirlem19  37679  poimirlem20  37680  poimirlem22  37682  poimirlem23  37683  poimirlem24  37684  poimirlem25  37685  poimirlem29  37689  poimirlem31  37691  ovoliunnfl  37702  voliunnfl  37704  volsupnfl  37705  ismtybndlem  37846  riccrng1  42554  ricdrng1  42561  kelac1  43096  gicabl  43132  imasubc  49183