Theorem foima 6766

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 6028	. 2 ⊢ (𝐹 “ dom 𝐹) = ran 𝐹
2		fof 6761	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
3	2	fdmd 6684	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 → dom 𝐹 = 𝐴)
4	3	imaeq2d 6018	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ dom 𝐹) = (𝐹 “ 𝐴))
5		forn 6764	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
6	1, 4, 5	3eqtr3a 2795	1 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ 𝐴) = 𝐵)

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5638  ran crn 5639   “ cima 5641  –onto→wfo 6499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-xp 5644  df-cnv 5646  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-fn 6504  df-f 6505  df-fo 6507

This theorem is referenced by:  foimacnv  6806  domunfican  9271  fiint  9275  fodomfi  9276  cantnflt2  9618  cantnfp1lem3  9625  enfin1ai  10329  symgfixelsi  19231  dprdf1o  19825  lmimlbs  21279  cncmp  22780  cmpfi  22796  cnconn  22810  qtopval2  23084  elfm3  23338  rnelfm  23341  fmfnfmlem2  23343  fmfnfm  23346  eupthvdres  29242  pjordi  31178  qtophaus  32506  poimirlem1  36152  poimirlem2  36153  poimirlem3  36154  poimirlem4  36155  poimirlem5  36156  poimirlem6  36157  poimirlem7  36158  poimirlem9  36160  poimirlem10  36161  poimirlem11  36162  poimirlem12  36163  poimirlem14  36165  poimirlem16  36167  poimirlem17  36168  poimirlem19  36170  poimirlem20  36171  poimirlem22  36173  poimirlem23  36174  poimirlem24  36175  poimirlem25  36176  poimirlem29  36180  poimirlem31  36182  ovoliunnfl  36193  voliunnfl  36195  volsupnfl  36196  ismtybndlem  36338  riccrng1  40770  ricdrng1  40778  kelac1  41448  gicabl  41484