Theorem ffn 3734

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 3275	. 2 ⊢ (F:A–→B ↔ (F Fn A ⋀ ran F ⊆ B))
2	1	pm3.26bi 320	1 ⊢ (F:A–→B → F Fn A)

Syntax hints:   → wi 3   ⊆ wss 2099  ran crn 3252   Fn wfn 3258  –→wf 3259

This theorem is referenced by:  dffn2 3735  ffun 3736  frel 3737  fdm 3738  fss 3742  fcoi1 3752  feu 3754  fex 3759  fofn 3781  dffo2 3783  f1ofn 3798  dff1o5 3805  f1f1orn 3807  fvco3 3887  ffvelrn 3928  dff2 3930  dffo3 3933  dffo4 3934  dffo5 3935  ffnfv 3942  fsn2 3950  fopabsn 3954  fconst2g 3959  fconstfv 3963  dff13 3988  fo1stres 4156  fo2ndres 4157  1stcof 4160  curry1f 4194  curry2f 4197  canth 4205  mapval2 4476  mapsn 4486  pw2en 4587  mapenlem2 4637  xpmapenlem3 4645  mapunen 4649  ac6s2 4904  carduniima 5040  cardinfima 5041  unirnioo 6529  dfioo2 6530  fsequb2 6655  fseqsupubi 6657  seq1ublem 7114  seq1ubi 7115  climsupi 7358  cvgcmpubi 7389  cncffvrn 7478  eff2 7575  ruclem33 7754  ruclem35 7756  ruclem37 7758  retopbas 7865  iooretop 7869  dnsconst 7998  blssioo 8124  tgioo 8126  lmsslem 8163  xplm 8186  bcthlem33 8242  issubgi 8364  vcoprnelem 8444  invfval 8508  cnnvm 8560  ip1cnilem2 8628  sspg 8641  ssps 8643  sspmlem 8645  sspn 8649  nvo00 8678  nmlno0lem 8708  lnon0 8713  phoeqi 8774  sinco 8934  cosco 8935  efghgrpilem 8991  hilnormi 9306  hhip 9320  hhssabli 9408  hhssnv 9410  hhsssh 9415  pjfn 9932  df0op2 9958  hoeq 9966  hocofni 9973  hoaddfni 9976  hosubfni 9977  hon0 9999  ho01i 10034  hoeq1 10036  kbpj 10160  nmlnop0iALT 10199  lnopco0i 10208  lnopconi 10242  lnfnconi 10269  cnvbraval 10323  hmopidmpji 10360  ghomgrpilem2 10671  ghomfo 10676  cayleylem2 10695  njtlc 10804  seqzp2 10918  bwt2 11123  intrn 11141  hartoglem 11435  cncls 11473  cnntr 11474  cnsubsp2 11484  compsub 11488  hscptsscld 11491  alexsub 11500  subtopmet 11506  2ndcctbss 11539  comppfsc 11578  cnpfillim 11686  elfilmap 11690  fmf 11693  fmbas 11694  filmapss 11696  rnelfmlem 11698  rnelfm 11699  fmfnfmlem2 11701  fmfnfm 11704  fcluscnplem 11729  tailuni 11761  tailfb 11762  filnetlem5 11767  filnet 11768  gafo 11773  gapm 11784  fnopabco 11810  oprabco 11811  f1elima 11818  upxp 11822  upixp 11823  indexd 11846  sdclem1 11875  sdclem2 11876  sdc 11877  cnimass 11949  cnres 11950  cnresima 11952  uptx 11978  txcnopab 11980  heiborlem33 12043  rrnmet 12072  phtpyid 12091  phtpycom 12092  phtpycolem3 12095  phtpycolem4 12096

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 145  df-an 223  df-f 3275

Copyright terms: Public domain