Theorem foima 6800

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 6059	. 2 ⊢ (𝐹 “ dom 𝐹) = ran 𝐹
2		fof 6795	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
3	2	fdmd 6718	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 → dom 𝐹 = 𝐴)
4	3	imaeq2d 6049	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ dom 𝐹) = (𝐹 “ 𝐴))
5		forn 6798	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
6	1, 4, 5	3eqtr3a 2788	1 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ 𝐴) = 𝐵)

Syntax hints:   → wi 4   = wceq 1533  dom cdm 5666  ran crn 5667   “ cima 5669  –onto→wfo 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pr 5417

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-br 5139  df-opab 5201  df-xp 5672  df-cnv 5674  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-fn 6536  df-f 6537  df-fo 6539

This theorem is referenced by:  foimacnv  6840  domunfican  9315  fiint  9319  fodomfi  9320  cantnflt2  9663  cantnfp1lem3  9670  enfin1ai  10374  symgfixelsi  19344  dprdf1o  19943  lmimlbs  21698  cncmp  23217  cmpfi  23233  cnconn  23247  qtopval2  23521  elfm3  23775  rnelfm  23778  fmfnfmlem2  23780  fmfnfm  23783  eupthvdres  29923  pjordi  31861  qtophaus  33271  poimirlem1  36945  poimirlem2  36946  poimirlem3  36947  poimirlem4  36948  poimirlem5  36949  poimirlem6  36950  poimirlem7  36951  poimirlem9  36953  poimirlem10  36954  poimirlem11  36955  poimirlem12  36956  poimirlem14  36958  poimirlem16  36960  poimirlem17  36961  poimirlem19  36963  poimirlem20  36964  poimirlem22  36966  poimirlem23  36967  poimirlem24  36968  poimirlem25  36969  poimirlem29  36973  poimirlem31  36975  ovoliunnfl  36986  voliunnfl  36988  volsupnfl  36989  ismtybndlem  37130  riccrng1  41553  ricdrng1  41559  kelac1  42260  gicabl  42296