Theorem frn 3633

Description: The range of a mapping.

Assertion

Ref	Expression
frn	|- (F:A-->B -> ran F (_ B)

Proof of Theorem frn

Step	Hyp	Ref	Expression
1		df-f 3194	. 2 |- (F:A-->B <-> (F Fn A /\ ran F (_ B))
2	1	pm3.27bi 326	1 |- (F:A-->B -> ran F (_ B)

Syntax hints:   -> wi 3   (_ wss 2047  ran crn 3171   Fn wfn 3177  -->wf 3178

This theorem is referenced by:  fss 3635  fco 3636  fssxp 3637  fimacnvdisj 3649  f00 3657  foconst 3683  f1dmex 3710  fimacnv 3810  ffvelrn 3814  rnssopab 3825  fnfvrnss 3830  1stcof 4101  map0b 4343  mapsn 4345  fodomr 4483  mapenlem2 4490  inf3lem7 4619  carduniima 4890  unirnioo 6402  fsequb2 6524  fseqsupcl 6525  fseqsupub 6526  seq1ublem 6911  climsup 7155  cvgcmpub 7185  ruclem17 7526  ruclem33 7542  cncfmet1 7906  grplactf1o 8098  ghsubgi 8138  hhssims 9145  kbass5t 10053  ghomgrpilem2 10386  ghomfo 10391  cayleylem2 10410  rdmob 10681  rcmob 10682

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-f 3194

Copyright terms: Public domain