Theorem foima 6747

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 6742	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
3	2	fdmd 6668	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 → dom 𝐹 = 𝐴)
4	3	imaeq2d 6018	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ dom 𝐹) = (𝐹 “ 𝐴))
5		forn 6745	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
6	1, 4, 5	3eqtr3a 2800	1 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ 𝐴) = 𝐵)

Syntax hints:   → wi 4   = wceq 1548  dom cdm 5620  ran crn 5621   “ cima 5623  –onto→wfo 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5220  ax-pr 5364

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-br 5075  df-opab 5137  df-xp 5626  df-cnv 5628  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-fn 6491  df-f 6492  df-fo 6494

This theorem is referenced by:  foimacnv  6787  fodomfi  9216  domunfican  9226  fiint  9231  fodomfiOLD  9234  cantnflt2  9589  cantnfp1lem3  9596  enfin1ai  10302  symgfixelsi  19404  dprdf1o  20003  lmimlbs  21814  cncmp  23378  cmpfi  23394  cnconn  23408  qtopval2  23682  elfm3  23936  rnelfm  23939  fmfnfmlem2  23941  fmfnfm  23944  eupthvdres  30325  pjordi  32264  qtophaus  34030  poimirlem1  38001  poimirlem2  38002  poimirlem3  38003  poimirlem4  38004  poimirlem5  38005  poimirlem6  38006  poimirlem7  38007  poimirlem9  38009  poimirlem10  38010  poimirlem11  38011  poimirlem12  38012  poimirlem14  38014  poimirlem16  38016  poimirlem17  38017  poimirlem19  38019  poimirlem20  38020  poimirlem22  38022  poimirlem23  38023  poimirlem24  38024  poimirlem25  38025  poimirlem29  38029  poimirlem31  38031  ovoliunnfl  38042  voliunnfl  38044  volsupnfl  38045  ismtybndlem  38186  riccrng1  43020  ricdrng1  43027  kelac1  43521  gicabl  43557  imasubc  49653