Theorem foima 6799

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 6067	. 2 ⊢ (𝐹 “ dom 𝐹) = ran 𝐹
2		fof 6794	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
3	2	fdmd 6718	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 → dom 𝐹 = 𝐴)
4	3	imaeq2d 6052	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ dom 𝐹) = (𝐹 “ 𝐴))
5		forn 6797	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
6	1, 4, 5	3eqtr3a 2820	1 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ 𝐴) = 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5651  ran crn 5652   “ cima 5654  –onto→wfo 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-fn 6540  df-f 6541  df-fo 6543

This theorem is used by:  foimacnv  6840  fodomfi  9297  domunfican  9306  fiint  9311  cantnflt2  9667  cantnfp1lem3  9674  enfin1ai  10455  symgfixelsi  19642  dprdf1o  20241  lmimlbs  22135  cncmp  23703  cmpfi  23719  cnconn  23733  qtopval2  24008  elfm3  24262  rnelfm  24265  fmfnfmlem2  24267  fmfnfm  24270  eupthvdres  30829  pjordi  32768  qtophaus  34461  poimirlem1  38519  poimirlem2  38520  poimirlem3  38521  poimirlem4  38522  poimirlem5  38523  poimirlem6  38524  poimirlem7  38525  poimirlem9  38527  poimirlem10  38528  poimirlem11  38529  poimirlem12  38530  poimirlem14  38532  poimirlem16  38534  poimirlem17  38535  poimirlem19  38537  poimirlem20  38538  poimirlem22  38540  poimirlem23  38541  poimirlem24  38542  poimirlem25  38543  poimirlem29  38547  poimirlem31  38549  ovoliunnfl  38560  voliunnfl  38562  volsupnfl  38563  ismtybndlem  38720  riccrng1  43562  ricdrng1  43572  kelac1  44049  gicabl  44085  imasubc  50228