Theorem frn 3639

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 3200	. 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 2050  ran crn 3177   Fn wfn 3183  -->wf 3184

This theorem is referenced by:  fss 3641  fco 3642  fssxp 3643  fimacnvdisj 3655  f00 3663  foconst 3689  f1dmex 3716  fimacnv 3816  ffvelrn 3820  rnssopab 3831  fnfvrnss 3836  1stcof 4107  map0b 4349  mapsn 4351  fodomr 4489  mapenlem2 4496  inf3lem7 4628  carduniima 4901  unirnioo 6403  fsequb2 6525  fseqsupcl 6526  fseqsupub 6527  seq1ublem 6911  climsup 7155  cvgcmpub 7185  ruclem17 7527  ruclem33 7543  cncfmet1 7903  grplactf1o 8094  ghsubgi 8134  hhssims 9140  kbass5t 10048  ghomgrpilem2 10381  ghomfo 10386  cayleylem2 10405  rdmob 10652  rcmob 10653

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 3200

Copyright terms: Public domain