Theorem forn 3674

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 3196	. 2 |- (F:A-onto->B <-> (F Fn A /\ ran F = B))
2	1	pm3.27bi 326	1 |- (F:A-onto->B -> ran F = B)

Syntax hints:   -> wi 3   = wceq 956  ran crn 3171   Fn wfn 3177  -onto->wfo 3180

This theorem is referenced by:  dffo2 3675  foima 3676  fornex 3679  fodmrnu 3680  f1imacnv 3705  f1ococnv2 3708  cbvfo 3885  isoini 3900  isofrlem 3901  canth 3907  curry1 4098  en1 4426  ssenen 4504  phplem4 4511  php3 4515  php3OLD 4516  ssfi 4537  ssfiOLD 4538  fodomfibOLD 4567  fodom 4798  fodomb 4800  unbenlem 7504  ruclem37 7546  infxpidmlem8 7559  infxpidmlem10 7561  infxpidmlem11 7562  infmap2lem2 7580  cnconst 7780  isgrp 8041  isgrpi 8042  isgrp2i 8076  vsfval 8254  pjrnt 9652  cayleylem3 10411

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-fo 3196

Copyright terms: Public domain