Theorem ffun 4565

Description: A mapping is a function.

Assertion

Ref	Expression
ffun	|- (F:A-->B -> Fun F)

Proof of Theorem ffun

Step	Hyp	Ref	Expression
1		ffn 4562	. 2 |- (F:A-->B -> F Fn A)
2		fnfun 4510	. 2 |- (F Fn A -> Fun F)
3	1, 2	syl 12	1 |- (F:A-->B -> Fun F)

Syntax hints:   -> wi 3  Fun wfun 3992   Fn wfn 3993  -->wf 3994

This theorem is referenced by:  fcoOLD 4574  funssxp 4577  f00 4601  fofun 4618  f1ores 4654  f1ococnv2 4662  fimacnv 4783  dff3 4790  ac6sfilem3 5508  fodomr 5547  mapenlem1 5583  ac6lem 5916  carduniima 6038  climuz0i 8368  dfef2i 8569  infxpidmlem7 8827  infmap2 8850  iscnp2 9037  cnpnei 9043  cnpco 9046  iscncl 9047  cnsscnp 9049  cncnplem4 9054  metcnplem 9164  metcnp 9165  metcnp3 9174  metcnss 9176  metcnss2 9177  cnmetdval 9180  bcthlem29 9305  ghsubgi 9446  gapmlem 9461  nvex 9562  imsdval 9649  sspg 9726  ssps 9728  sspn 9734  lnocoi 9757  sincolem 10014  tx1cn 10223  tx2cn 10224  upxp 10225  uptx 10226  txcnopab 10228  2txcn 10229  subtopmetlem 10255  subtopmet 10256  fmf 10310  fmbas 10311  elfilmap 10312  hocoi 11327  homco1 11364  homco2 11538  lnopcoi 11565  hmopco 11585  leopsq 11700  algrp1 13742  algcvg 13744  orderseqlem 13953  nofun 13993  njtlc 14389  injrec 14461  surjsec 14462  surjsec2 14467  seqzp2 14716  curgrpact 14735  svs3 14830  bwt2 14960  lvsovso 15038  supnuf 15041  rdmob 15095  rcmob 15096  idsubidsup 15205  idsubfun 15206  cncls 15419  cnsubsp 15426  cnsubsp2 15427  ivthALT 15454  cnpfillim 15589  rnelfmlem 15592  rnelfm 15593  fmfnfmlem2 15595  fmfnfmlem3 15596  fmfnfmlem4 15597  fmfnfm 15598  foco2 15686  cocanfo 15689  fnopabco 15711  upixp 15729  indexdom 15754  cnss 15892  paste 15893  heiborlem14 15968  heiborlem15 15969  heiborlem33 15987  heiborlem34 15988  ghomco 16040  grpkerinj 16042  reparpht 16065  pcocn 16076  rnghomco 16128

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 164  df-an 242  df-fn 4009  df-f 4010

Copyright terms: Public domain