Theorem foima 6802

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 6066	. 2 ⊢ (𝐹 “ dom 𝐹) = ran 𝐹
2		fof 6797	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
3	2	fdmd 6721	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 → dom 𝐹 = 𝐴)
4	3	imaeq2d 6051	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ dom 𝐹) = (𝐹 “ 𝐴))
5		forn 6800	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
6	1, 4, 5	3eqtr3a 2819	1 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ 𝐴) = 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1569  dom cdm 5650  ran crn 5651   “ cima 5653  –onto→wfo 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5656  df-cnv 5658  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-fn 6542  df-f 6543  df-fo 6545

This theorem is used by:  foimacnv  6843  fodomfi  9308  domunfican  9317  fiint  9322  cantnflt2  9678  cantnfp1lem3  9685  enfin1ai  10466  symgfixelsi  19655  dprdf1o  20254  lmimlbs  22148  cncmp  23716  cmpfi  23732  cnconn  23746  qtopval2  24021  elfm3  24275  rnelfm  24278  fmfnfmlem2  24280  fmfnfm  24283  eupthvdres  30842  pjordi  32781  qtophaus  34515  poimirlem1  38633  poimirlem2  38634  poimirlem3  38635  poimirlem4  38636  poimirlem5  38637  poimirlem6  38638  poimirlem7  38639  poimirlem9  38641  poimirlem10  38642  poimirlem11  38643  poimirlem12  38644  poimirlem14  38646  poimirlem16  38648  poimirlem17  38649  poimirlem19  38651  poimirlem20  38652  poimirlem22  38654  poimirlem23  38655  poimirlem24  38656  poimirlem25  38657  poimirlem29  38661  poimirlem31  38663  ovoliunnfl  38674  voliunnfl  38676  volsupnfl  38677  ismtybndlem  38834  riccrng1  43676  ricdrng1  43686  kelac1  44159  gicabl  44195  imasubc  50361