Theorem forn 2789

Description: The codomain of an onto function is its range.

Assertion

Ref	Expression
forn	|- (F:A-onto->B -> ran F = B)

Proof of Theorem forn

Step	Hyp	Ref	Expression
1		df-fo 2436	. 2 |- (F:A-onto->B <-> (F Fn A /\ ran F = B))
2	1	pm3.27bd 263	1 |- (F:A-onto->B -> ran F = B)

Syntax hints:   -> wi 2   = wceq 1091  ran crn 2411   Fn wfn 2417  -onto->wfo 2420

This theorem is referenced by:  foima 2790  fornex 2793  f1imacnv 2814  f1ococnv2 2817  cbvfo 2923  isoini 2938  isofrlem 2939  canth 2945  en1 3331  ssenen 3399  phplem5 3407  php3 3411  ssfi 3430  fodom 3613  fodomb 3615  ruclem37 4921  infxpidmlem8 4940  infxpidmlem10 4942  infxpidmlem11 4943  infmap2lem2 4952

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198  df-fo 2436

metamath.org