Theorem ffun 3635

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 3633	. 2 |- (F:A-->B -> F Fn A)
2		fnfun 3591	. 2 |- (F Fn A -> Fun F)
3	1, 2	syl 10	1 |- (F:A-->B -> Fun F)

Syntax hints:   -> wi 3  Fun wfun 3182   Fn wfn 3183  -->wf 3184

This theorem is referenced by:  fco 3642  funssxp 3644  f00 3663  fofun 3679  f1ores 3709  f1ococnv2 3714  fimacnv 3816  dff2 3823  fodomr 4489  mapenlem1 4495  ac6lem 4764  carduniima 4901  climuz0 7108  dfef2 7307  infxpidmlem7 7559  infmap2 7583  iscnp2 7758  cnpco 7766  iscncl 7767  cnsscnp 7769  cncnplem4 7774  metcnplem 7883  metcnp 7884  metcnp3 7893  metcnss 7895  metcnss2 7896  cnmetdval 7899  bcthlem29 8024  ghsubgi 8134  nvex 8226  imsdval 8313  sspg 8383  ssps 8385  sspn 8391  lnocoi 8414  sincolem 8660  hoco 9685  homco1t 9722  homco2t 9896  lnopco 9923  hmopcot 9943  leopsqt 10057  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-fn 3199  df-f 3200

Copyright terms: Public domain