Theorem ffn 3613

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 3184	. 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 2037  ran crn 3161   Fn wfn 3167  -->wf 3168

This theorem is referenced by:  fnf 3614  ffun 3615  frel 3616  fdm 3617  fss 3620  fcoi1 3630  feu 3632  fex 3637  dffo2 3660  fodmrnu 3665  f1ofn 3675  f1o5 3682  f1f1orn 3684  fo00 3700  fvco3 3761  ffvelrn 3799  dff4 3801  dffo3 3804  dffo4 3805  dffo5 3806  ffnfv 3813  fsn2 3821  fopabsn 3825  fconst2g 3830  fconstfv 3834  f1fv 3859  canth 3892  2ndconst 4081  curry1f 4083  1stcof 4085  df1st2 4110  df2nd2 4111  mapval2 4319  mapsn 4329  pw2en 4426  mapenlem2 4470  xpmapenlem3 4478  mapunen 4482  fodomfi 4540  ac6s2 4730  carduniima 4862  cardinfima 4863  unirnioo 6335  dfioo2 6336  fsequb2 6456  fseqsupub 6458  seq1ublem 6848  seq1ub 6849  climsup 7091  cvgcmpub 7121  cncffvrn 7208  eff2 7312  ruclem33 7485  ruclem35 7487  ruclem37 7489  infmap2lem2 7522  retopbas 7597  iooretop 7601  dnsconst 7727  blssioo 7852  tgioo 7854  lmsslem 7887  xplm 7909  bcthlem33 7965  grprn 7990  resgrprnOLD 8031  subgres 8054  issubgi 8059  vcoprnelem 8135  0vfval 8163  invfval 8201  cnnvm 8251  ip1cnilem2 8308  sspg 8321  ssps 8323  sspmlem 8325  sspn 8329  nvo00 8356  nmlno0lem 8385  phoeqi 8449  sinco 8586  cosco 8587  efghgrpilem 8634  circgrpOLD 8658  hilnorm 8951  hhip 8965  hhssabl 9053  hhssnv 9054  hhsssh 9059  pjfnt 9571  df0op2 9595  hoeqt 9603  hocofn 9610  hoaddfn 9613  hosubfn 9614  hon0 9636  ho01 9671  hoeq1t 9673  kbpjt 9796  nmlnop0ALT 9835  lnopco0 9844  lnopcon 9878  lnfncon 9905  cnvbravalt 9956  hmopidmpj 9991  ghomgrpilem2 10291  ghomfo 10296  cayleylem2 10317  cayleylem3 10318

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 3184

Copyright terms: Public domain