Theorem ffun 3629

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

Syntax hints:   -> wi 3  Fun wfun 3176   Fn wfn 3177  -->wf 3178

This theorem is referenced by:  fco 3636  funssxp 3638  f00 3657  fofun 3673  f1ores 3703  f1ococnv2 3708  fimacnv 3810  dff2 3817  fodomr 4483  mapenlem1 4489  ac6lem 4754  carduniima 4890  climuz0 7108  dfef2 7307  infxpidmlem7 7558  infmap2 7581  iscnp2 7761  cnpco 7769  iscncl 7770  cnsscnp 7772  cncnplem4 7777  metcnplem 7886  metcnp 7887  metcnp3 7896  metcnss 7898  metcnss2 7899  cnmetdval 7902  bcthlem29 8027  ghsubgi 8138  nvex 8230  imsdval 8317  sspg 8387  ssps 8389  sspn 8395  lnocoi 8418  sincolem 8665  hoco 9690  homco1t 9727  homco2t 9901  lnopco 9928  hmopcot 9948  leopsqt 10062  rdmob 10681  rcmob 10682

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 3193  df-f 3194

Copyright terms: Public domain