Theorem ffn 3627

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 3194	. 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 2047  ran crn 3171   Fn wfn 3177  -->wf 3178

This theorem is referenced by:  fnf 3628  ffun 3629  frel 3630  fdm 3631  fss 3635  fcoi1 3645  feu 3647  fex 3652  dffo2 3675  fodmrnu 3680  f1ofn 3690  f1o5 3697  f1f1orn 3699  fo00 3715  fvco3 3776  ffvelrn 3814  dff4 3816  dffo3 3819  dffo4 3820  dffo5 3821  ffnfv 3828  fsn2 3836  fopabsn 3840  fconst2g 3845  fconstfv 3849  f1fv 3874  canth 3907  2ndconst 4097  curry1f 4099  1stcof 4101  df1st2 4126  df2nd2 4127  mapval2 4335  mapsn 4345  pw2en 4446  mapenlem2 4490  xpmapenlem3 4498  mapunen 4502  fodomfiOLD 4566  ac6s2 4758  carduniima 4890  cardinfima 4891  unirnioo 6402  dfioo2 6403  fsequb2 6524  fseqsupub 6526  seq1ublem 6911  seq1ub 6912  climsup 7155  cvgcmpub 7185  cncffvrn 7273  eff2 7370  ruclem33 7542  ruclem35 7544  ruclem37 7546  infmap2lem2 7580  retopbas 7655  iooretop 7659  dnsconst 7788  blssioo 7913  tgioo 7915  lmsslem 7952  xplm 7975  bcthlem33 8031  grprn 8056  subgres 8117  issubgi 8122  vcoprnelem 8197  0vfval 8225  invfval 8261  cnnvm 8313  ip1cnilem2 8374  sspg 8387  ssps 8389  sspmlem 8391  sspn 8395  nvo00 8424  nmlno0lem 8453  lnon0 8458  phoeqi 8518  sinco 8667  cosco 8668  efghgrpilem 8719  hilnorm 9030  hhip 9044  hhssabl 9132  hhssnv 9134  hhsssh 9139  pjfnt 9654  df0op2 9678  hoeqt 9686  hocofn 9693  hoaddfn 9696  hosubfn 9697  hon0 9719  ho01 9754  hoeq1t 9756  kbpjt 9880  nmlnop0ALT 9920  lnopco0 9929  lnopcon 9963  lnfncon 9990  cnvbravalt 10043  hmopidmpj 10080  ghomgrpilem2 10386  ghomfo 10391  cayleylem2 10410  cayleylem3 10411

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 3194

Copyright terms: Public domain