Theorem foima 6744

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 6022	. 2 ⊢ (𝐹 “ dom 𝐹) = ran 𝐹
2		fof 6739	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
3	2	fdmd 6665	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 → dom 𝐹 = 𝐴)
4	3	imaeq2d 6012	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ dom 𝐹) = (𝐹 “ 𝐴))
5		forn 6742	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
6	1, 4, 5	3eqtr3a 2798	1 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ 𝐴) = 𝐵)

Syntax hints:   → wi 4   = wceq 1547  dom cdm 5618  ran crn 5619   “ cima 5621  –onto→wfo 6483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-xp 5624  df-cnv 5626  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-fn 6488  df-f 6489  df-fo 6491

This theorem is referenced by:  foimacnv  6784  fodomfi  9212  domunfican  9222  fiint  9227  fodomfiOLD  9230  cantnflt2  9585  cantnfp1lem3  9592  enfin1ai  10297  symgfixelsi  19401  dprdf1o  20000  lmimlbs  21811  cncmp  23375  cmpfi  23391  cnconn  23405  qtopval2  23679  elfm3  23933  rnelfm  23936  fmfnfmlem2  23938  fmfnfm  23941  eupthvdres  30323  pjordi  32262  qtophaus  34020  poimirlem1  37988  poimirlem2  37989  poimirlem3  37990  poimirlem4  37991  poimirlem5  37992  poimirlem6  37993  poimirlem7  37994  poimirlem9  37996  poimirlem10  37997  poimirlem11  37998  poimirlem12  37999  poimirlem14  38001  poimirlem16  38003  poimirlem17  38004  poimirlem19  38006  poimirlem20  38007  poimirlem22  38009  poimirlem23  38010  poimirlem24  38011  poimirlem25  38012  poimirlem29  38016  poimirlem31  38018  ovoliunnfl  38029  voliunnfl  38031  volsupnfl  38032  ismtybndlem  38173  riccrng1  43007  ricdrng1  43014  kelac1  43508  gicabl  43544  imasubc  49641