Theorem ffn 3633

Description: A mapping is a function.

Assertion

Ref	Expression
ffn	|- (F:A-->B -> F Fn A)

Proof of Theorem ffn

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

Syntax hints:   -> wi 3   (_ wss 2050  ran crn 3177   Fn wfn 3183  -->wf 3184

This theorem is referenced by:  fnf 3634  ffun 3635  frel 3636  fdm 3637  fss 3641  fcoi1 3651  feu 3653  fex 3658  dffo2 3681  fodmrnu 3686  f1ofn 3696  f1o5 3703  f1f1orn 3705  fo00 3721  fvco3 3782  ffvelrn 3820  dff4 3822  dffo3 3825  dffo4 3826  dffo5 3827  ffnfv 3834  fsn2 3842  fopabsn 3846  fconst2g 3851  fconstfv 3855  f1fv 3880  canth 3913  2ndconst 4103  curry1f 4105  1stcof 4107  df1st2 4132  df2nd2 4133  mapval2 4341  mapsn 4351  pw2en 4452  mapenlem2 4496  xpmapenlem3 4504  mapunen 4508  fodomfi 4575  fodomfiOLD 4576  ac6s2 4768  carduniima 4901  cardinfima 4902  unirnioo 6403  dfioo2 6404  fsequb2 6525  fseqsupub 6527  seq1ublem 6911  seq1ub 6912  climsup 7155  cvgcmpub 7185  cncffvrn 7273  eff2 7370  ruclem33 7543  ruclem35 7545  ruclem37 7547  infmap2lem2 7582  retopbas 7652  iooretop 7656  dnsconst 7785  blssioo 7910  tgioo 7912  lmsslem 7949  xplm 7972  bcthlem33 8028  grprn 8053  subgres 8113  issubgi 8118  vcoprnelem 8193  0vfval 8221  invfval 8257  cnnvm 8309  ip1cnilem2 8370  sspg 8383  ssps 8385  sspmlem 8387  sspn 8391  nvo00 8420  nmlno0lem 8449  lnon0 8454  phoeqi 8514  sinco 8662  cosco 8663  efghgrpilem 8714  hilnorm 9025  hhip 9039  hhssabl 9127  hhssnv 9129  hhsssh 9134  pjfnt 9649  df0op2 9673  hoeqt 9681  hocofn 9688  hoaddfn 9691  hosubfn 9692  hon0 9714  ho01 9749  hoeq1t 9751  kbpjt 9875  nmlnop0ALT 9915  lnopco0 9924  lnopcon 9958  lnfncon 9985  cnvbravalt 10038  hmopidmpj 10075  ghomgrpilem2 10381  ghomfo 10386  cayleylem2 10405  cayleylem3 10406

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