Theorem foima 6780

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 6044	. 2 ⊢ (𝐹 “ dom 𝐹) = ran 𝐹
2		fof 6775	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
3	2	fdmd 6701	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 → dom 𝐹 = 𝐴)
4	3	imaeq2d 6034	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ dom 𝐹) = (𝐹 “ 𝐴))
5		forn 6778	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
6	1, 4, 5	3eqtr3a 2789	1 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ 𝐴) = 𝐵)

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5641  ran crn 5642   “ cima 5644  –onto→wfo 6512

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-cnv 5649  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-fn 6517  df-f 6518  df-fo 6520

This theorem is referenced by:  foimacnv  6820  fodomfi  9268  domunfican  9279  fiint  9284  fiintOLD  9285  fodomfiOLD  9288  cantnflt2  9633  cantnfp1lem3  9640  enfin1ai  10344  symgfixelsi  19372  dprdf1o  19971  lmimlbs  21752  cncmp  23286  cmpfi  23302  cnconn  23316  qtopval2  23590  elfm3  23844  rnelfm  23847  fmfnfmlem2  23849  fmfnfm  23852  eupthvdres  30171  pjordi  32109  qtophaus  33833  poimirlem1  37622  poimirlem2  37623  poimirlem3  37624  poimirlem4  37625  poimirlem5  37626  poimirlem6  37627  poimirlem7  37628  poimirlem9  37630  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem14  37635  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem22  37643  poimirlem23  37644  poimirlem24  37645  poimirlem25  37646  poimirlem29  37650  poimirlem31  37652  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  ismtybndlem  37807  riccrng1  42516  ricdrng1  42523  kelac1  43059  gicabl  43095  imasubc  49144