Theorem foima 6777

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 6041	. 2 ⊢ (𝐹 “ dom 𝐹) = ran 𝐹
2		fof 6772	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
3	2	fdmd 6698	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 → dom 𝐹 = 𝐴)
4	3	imaeq2d 6031	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ dom 𝐹) = (𝐹 “ 𝐴))
5		forn 6775	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
6	1, 4, 5	3eqtr3a 2788	1 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ 𝐴) = 𝐵)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-cnv 5646  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-fn 6514  df-f 6515  df-fo 6517

This theorem is referenced by:  foimacnv  6817  fodomfi  9261  domunfican  9272  fiint  9277  fiintOLD  9278  fodomfiOLD  9281  cantnflt2  9626  cantnfp1lem3  9633  enfin1ai  10337  symgfixelsi  19365  dprdf1o  19964  lmimlbs  21745  cncmp  23279  cmpfi  23295  cnconn  23309  qtopval2  23583  elfm3  23837  rnelfm  23840  fmfnfmlem2  23842  fmfnfm  23845  eupthvdres  30164  pjordi  32102  qtophaus  33826  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem4  37618  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem9  37623  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem14  37628  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem22  37636  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem29  37643  poimirlem31  37645  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  ismtybndlem  37800  riccrng1  42509  ricdrng1  42516  kelac1  43052  gicabl  43088  imasubc  49140