Theorem ffn 6662

Description: A mapping is a function with domain. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
ffn	⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)

Proof of Theorem ffn

Step	Hyp	Ref	Expression
1		df-f 6496	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2	1	simplbi 497	1 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   ⊆ wss 3901  ran crn 5625   Fn wfn 6487  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-f 6496

This theorem is referenced by:  ffnd  6663  ffun  6665  frel  6667  fdm  6671  ffrn  6675  fresin  6703  fresaun  6705  fresaunres2  6706  fcoi1  6708  feu  6710  f0bi  6717  dffo2  6750  fimadmfo  6755  fdmeu  6890  feqmptdf  6904  fimarab  6908  fvco3  6933  ffvelcdm  7026  dff2  7044  dffo3  7047  dffo4  7048  dffo5  7049  dffo3f  7051  f1ompt  7056  ffnfv  7064  fcdmssb  7067  fcompt  7078  fsn2  7081  fprb  7140  fconst2g  7149  fpr2g  7157  fex  7172  dff13  7200  nvocnv  7227  soisores  7273  fdmexb  7849  resf1extb  7876  fo1stres  7959  fo2ndres  7960  1stcof  7963  2ndcof  7964  curry1f  8048  curry2f  8050  fparlem1  8054  fparlem2  8055  fo2ndf  8063  soseq  8101  tposf2  8192  smo11  8296  fsetexb  8801  mapsnd  8824  pw2f1olem  9009  mapen  9069  mapunen  9074  fissuni  9257  fipreima  9258  indexfi  9260  mapfien  9311  oismo  9445  cantnflt  9581  cantnfp1lem3  9589  cantnflem4  9601  tcrank  9796  updjudhcoinlf  9844  updjudhcoinrg  9845  updjud  9846  infpwfien  9972  cardinfima  10007  dfacacn  10052  cfflb  10169  cofsmo  10179  cfcoflem  10182  coftr  10183  fin23lem40  10261  axdc3lem2  10361  ac6num  10389  ac6c4  10391  ac6s2  10396  ttukeylem6  10424  iunfo  10449  pwcfsdom  10494  fpwwe2lem5  10546  fpwwe2lem7  10548  pwfseqlem3  10571  inar1  10686  tskcard  10692  tskuni  10694  tskurn  10700  gruima  10713  nqerrel  10843  recmulnq  10875  dmrecnq  10879  axpre-sup  11080  ofsubeq0  12142  dfz2  12507  uzn0  12768  rpnnen1lem3  12892  rpnnen1lem5  12894  unirnioo  13365  dfioo2  13366  ioorebas  13367  fseq1p1m1  13514  2ffzeq  13565  fvinim0ffz  13705  injresinjlem  13706  fsequb2  13899  fseqsupcl  13900  fseqsupubi  13901  ser0f  13978  hashgval  14256  hashinf  14258  hashresfn  14263  ffz0hash  14370  fnfzo0hash  14373  wrdred1hash  14484  revlen  14685  revrev  14690  repswlen  14699  repsdf2  14701  cshword  14714  0csh0  14716  lenco  14755  s1co  14756  cshco  14759  swrdco  14760  s7f1o  14889  ofccat  14892  shftf  15002  uzin2  15268  rexanuz  15269  limsuple  15401  limsupval2  15403  rlimres  15481  lo1res  15482  rlimresb  15488  isercolllem2  15589  isercolllem3  15590  isercoll  15591  supcvg  15779  prodf1f  15815  eff2  16024  reeff1  16045  tanval  16053  ruclem4  16159  ruclem12  16166  prmreclem6  16849  1arithlem4  16854  1arith  16855  vdwmc  16906  vdwlem1  16909  vdwlem8  16916  vdwlem13  16921  ramval  16936  0ram  16948  0ram2  16949  0ramcl  16951  ramcl  16957  fsets  17096  firest  17352  0ssc  17761  0subcat  17762  isfull2  17837  arwhoma  17969  gsumval2a  18610  isgrpinv  18923  kerf1ghm  19176  f1omvdconj  19375  pmtrmvd  19385  pmtrfinv  19390  pmtrdifellem4  19408  efgsfo  19668  efgredlem  19676  efgcpbllemb  19684  frgpup3lem  19706  0frgp  19708  gexex  19782  torsubg  19783  gsumval3  19836  gsumzres  19838  gsummptmhm  19869  gsumzoppg  19873  dprdf1o  19963  dprd2db  19974  zrinitorngc  20575  zrtermorngc  20576  zrtermoringc  20608  srngf1o  20781  lmhmima  20999  lmhmpreima  21000  lmhmrnlss  21002  lspextmo  21008  pwssplit1  21011  cnfldadd  21315  cnfldmul  21317  dfcnfldOLD  21325  cnfldplusf  21351  cnfldsub  21352  chrrhm  21486  znunit  21518  psgnevpmb  21542  psgndiflemB  21555  mpofrlmd  21732  frlmipval  21734  frlmphl  21736  frlmlbs  21752  frlmup4  21756  ellspd  21757  lindfmm  21782  lsslindf  21785  psrbaglefi  21882  psrlidm  21917  mplmonmul  21991  evlseu  22038  mpfconst  22064  mpfproj  22065  mpfsubrg  22066  coe1sclmulfv  22225  pf1const  22290  pf1id  22291  pf1subrg  22292  mpfpf1  22295  pf1mpf  22296  mamuass  22346  mamudi  22347  mamudir  22348  mamuvs1  22349  mamuvs2  22350  1mavmul  22492  mavmulass  22493  mdetunilem7  22562  madutpos  22586  lecldbas  23163  lmbr2  23203  cncnpi  23222  cncnp  23224  cnpdis  23237  lmff  23245  pnrmopn  23287  dnsconst  23322  cmpsub  23344  tgcmp  23345  hauscmplem  23350  2ndcctbss  23399  2ndcomap  23402  2ndcsep  23403  1stccnp  23406  kgenidm  23491  iskgen2  23492  1stckgen  23498  kgen2cn  23503  ptpjpre1  23515  pttop  23526  ptuni  23538  ptval2  23545  tx1cn  23553  tx2cn  23554  ptpjcn  23555  ptpjopn  23556  ptclsg  23559  ptcnplem  23565  upxp  23567  txcnmpt  23568  uptx  23569  txcmplem2  23586  txkgen  23596  xkoptsub  23598  xkopt  23599  xkococnlem  23603  xkococn  23604  ptcmpfi  23757  zfbas  23840  uzrest  23841  rnelfmlem  23896  rnelfm  23897  fmfnfmlem2  23899  fmfnfm  23902  lmflf  23949  alexsubALT  23995  clssubg  24053  qustgplem  24065  tsmsres  24088  tsmsxplem1  24097  ucncn  24228  xmettpos  24293  imasdsf1olem  24317  blrnps  24352  blrn  24353  xmeterval  24376  tmslem  24426  tmsxms  24430  imasf1oxms  24433  prdsxms  24474  blval2  24506  metuel2  24509  isngp2  24541  isngp3  24542  tngngp2  24596  isnghm  24667  qtopbaslem  24702  qdensere  24713  cnbl0  24717  cnblcld  24718  cnfldms  24719  blssioo  24739  tgioo  24740  tgqioo  24744  xrtgioo  24751  xrsdsre  24755  xrge0tsms  24779  iimulcnOLD  24891  bndth  24913  lebnumlem3  24918  nmhmcn  25076  cphsqrtcl  25140  lmmbr2  25215  caucfil  25239  causs  25254  lmcau  25269  bcth3  25287  cncms  25311  cnfldcusp  25313  rrxmvallem  25360  ivthicc  25415  ovolfioo  25424  ovolficc  25425  ovolficcss  25426  ovollb2lem  25445  ovoliunlem2  25460  ovolshftlem1  25466  ovolicc2  25479  ismbl  25483  voliunlem2  25508  volsup  25513  ioorf  25530  ioorinv  25533  ioorcl  25534  uniiccdif  25535  uniioovol  25536  uniiccvol  25537  uniioombllem2  25540  uniioombllem4  25543  dyaddisj  25553  dyadmax  25555  dyadmbllem  25556  dyadmbl  25557  opnmbllem  25558  opnmblALT  25560  volsup2  25562  mbfdm  25583  mbfima  25587  mbfid  25592  ismbfd  25596  mbfres2  25602  mbfposr  25609  mbfimaopnlem  25612  mbflimsup  25623  0plef  25629  i1f1lem  25646  itg11  25648  itg1addlem4  25656  i1fpos  25663  itg1le  25670  itg1climres  25671  mbfi1fseqlem5  25676  mbfi1flimlem  25679  xrge0f  25688  itg2ge0  25692  itg2seq  25699  itg2i1fseqle  25711  itg2i1fseq2  25713  itg2addlem  25715  itg2gt0  25717  limciun  25851  dvres  25868  dvres3a  25871  cpnres  25895  dvfre  25911  dvmptres3  25916  dvlip2  25956  dvgt0lem2  25964  deg1fvi  26046  uc1pmon1p  26113  fta1g  26131  ig1peu  26136  ig1pdvds  26141  plyco0  26153  plypf1  26173  dgrlem  26190  dgrub  26195  dgrlb  26197  coemulc  26216  plyreres  26246  plydivlem3  26259  plydivlem4  26260  plydiveu  26262  plyremlem  26268  fta1lem  26271  fta1  26272  vieta1lem2  26275  plyexmo  26277  elaa  26280  elqaalem3  26285  aannenlem1  26292  pserulm  26387  psercnlem2  26390  psercnlem1  26391  psercn  26392  abelth  26407  reeff1o  26413  pilem1  26417  recosf1o  26500  resinf1o  26501  efif1olem3  26509  efif1olem4  26510  efifo  26512  eff1olem  26513  ellogrn  26524  logcn  26612  dvloglem  26613  logf1o2  26615  efopnlem1  26621  efopnlem2  26622  efopn  26623  logtayl  26625  cxpcn3lem  26713  cxpcn3  26714  resqrtcn  26715  asinneg  26852  areambl  26924  emcllem7  26968  lgamgulm2  27002  basellem4  27050  sqff1o  27148  mpodvdsmulf1o  27160  fsumdvdsmul  27161  dvdsmulf1o  27162  fsumdvdsmulOLD  27163  ostthlem1  27594  ostth  27606  noetasuplem4  27704  madeval2  27829  elold  27855  old1  27861  madeoldsuc  27881  tglnfn  28619  f1otrg  28943  axlowdimlem6  29020  axlowdimlem8  29022  axlowdimlem9  29023  axlowdimlem11  29025  axlowdimlem12  29026  axlowdimlem17  29031  elntg2  29058  dfpth2  29802  cyclnumvtx  29873  crctcshlem4  29893  clwlkclwwlklem2  30075  eucrct2eupth  30320  ex-fpar  30537  cnnvm  30757  sspmlem  30807  nvo00  30836  nmlno0lem  30868  phoeqi  30932  ubthlem1  30945  hhip  31252  hhssabloilem  31336  hhssnv  31339  hhsssh  31344  occllem  31378  shsel  31389  chscllem2  31713  df0op2  31827  hoeq  31835  hocofni  31842  hoaddfni  31845  hosubfni  31846  hon0  31868  ho01i  31903  hoeq1  31905  elnlfn  32003  nmlnop0iALT  32070  lnopco0i  32079  imaelshi  32133  nlelchi  32136  rnbra  32182  cnvbraval  32185  kbass5  32195  hmopidmchi  32226  hmopidmpji  32227  foresf1o  32579  fcomptf  32736  ofpreima  32743  resf1o  32809  maprnin  32810  fpwrelmapffslem  32811  hashgt1  32888  indpi1  32941  indpreima  32947  s3clhash  33030  gsumpart  33146  xrge0tsmsd  33155  tocyc01  33200  cyc3evpm  33232  cycpmgcl  33235  cycpmconjslem2  33237  cyc3conja  33239  kerunit  33406  1arithidomlem1  33616  1arithidomlem2  33617  1arithidom  33618  dimval  33757  dimvalfi  33758  ply1degltdimlem  33779  ply1degltdim  33780  elirng  33843  txomap  33991  locfinreflem  33997  hauseqcn  34055  xpinpreima  34063  xpinpreima2  34064  tpr2rico  34069  mndpluscn  34083  raddcn  34086  xrge0pluscn  34097  xrge0tmdALT  34103  rge0scvg  34106  pl1cn  34112  elzrhunit  34134  qqhf  34143  cnrrext  34167  qqhre  34177  1stmbfm  34417  2ndmbfm  34418  mbfmcnt  34425  omssubadd  34457  carsggect  34475  eulerpartlemsv2  34515  eulerpartlems  34517  eulerpartlemv  34521  eulerpartlemb  34525  eulerpartlemf  34527  eulerpartlemt  34528  eulerpartlemmf  34532  eulerpartlemgvv  34533  eulerpartlemgh  34535  eulerpartlemgs2  34537  sseqmw  34548  sseqf  34549  sseqp1  34552  fiblem  34555  fibp1  34558  plymul02  34703  signsvtn0  34727  signstres  34732  signshlen  34747  reprinrn  34775  circlemethhgt  34800  txsconnlem  35434  iccllysconn  35444  rellysconn  35445  cvmseu  35470  cvmliftmolem2  35476  cvmliftlem6  35484  cvmliftlem7  35485  cvmliftlem8  35486  cvmliftlem9  35487  cvmliftlem11  35489  cvmliftlem15  35492  cvmlift2lem7  35503  cvmlift2lem10  35506  cvmlift3lem8  35520  cvmlift3lem9  35521  mvrsfpw  35700  mrsubff1  35708  msrid  35739  msrfo  35740  elmsta  35742  mtyf  35746  msubff1  35750  vhmcls  35760  mclsax  35763  elmthm  35770  mthmblem  35774  mclsppslem  35777  iprodefisumlem  35934  fullfunfnv  36140  fullfunfv  36141  tailfb  36571  filnetlem4  36575  regsfromunir1  36670  taupilem3  37524  icoreresf  37557  icoreelrnab  37559  relowlssretop  37568  relowlpssretop  37569  unccur  37804  matunitlindflem1  37817  matunitlindflem2  37818  ptrecube  37821  poimirlem28  37849  poimirlem32  37853  heicant  37856  opnmbllem0  37857  mblfinlem1  37858  mblfinlem2  37859  volsupnfl  37866  cnambfre  37869  dvtan  37871  itg2addnclem  37872  itg2addnclem2  37873  ftc1anclem3  37896  ftc1anclem5  37898  ftc1anclem7  37900  ftc1anclem8  37901  ftc1anc  37902  areacirc  37914  indexdom  37935  sdclem2  37943  sstotbnd2  37975  sstotbnd  37976  isbndx  37983  isbnd3b  37986  prdsbnd  37994  prdstotbnd  37995  ismtyhmeolem  38005  heibor1lem  38010  heiborlem1  38012  heibor  38022  rrnequiv  38036  keridl  38233  ellkr  39349  lkr0f  39354  cdleme50rnlem  40804  aks6d1c2lem4  42381  aks6d1c5  42393  sticksstones11  42410  sticksstones19  42419  sticksstones22  42422  aks6d1c6lem4  42427  aks6d1c6isolem2  42429  fsuppind  42833  elrfirn  42937  ismrcd2  42941  isnacs2  42948  nacsfix  42954  mapfzcons1  42959  mzpcompact2lem  42993  eq0rabdioph  43018  eldioph4b  43053  diophren  43055  pw2f1ocnv  43279  pw2f1o2val2  43282  lmhmfgsplit  43328  pwssplit4  43331  hbt  43372  mpaaeu  43392  mendring  43430  proot1mul  43436  proot1hash  43437  proot1ex  43438  deg1mhm  43442  fgraphopab  43445  hausgraph  43447  nvocnvb  43663  ofsubid  44565  expgrowthi  44574  expgrowth  44576  binomcxplemdvbinom  44594  binomcxplemcvg  44595  binomcxplemnotnn0  44597  relpfrlem  45194  rfcnpre1  45264  rfcnpre2  45276  cncmpmax  45277  rfcnpre3  45278  rfcnpre4  45279  elixpconstg  45333  ffi  45417  islptre  45865  resincncf  46119  dvcosre  46156  dvresntr  46162  volioof  46231  stoweidlem48  46292  fourierdlem12  46363  fourierdlem15  46366  fourierdlem41  46392  fourierdlem42  46393  fourierdlem46  46396  fourierdlem48  46398  fourierdlem49  46399  fourierdlem54  46404  fourierdlem56  46406  fourierdlem62  46412  fourierdlem64  46414  fourierdlem65  46415  fourierdlem73  46423  fourierdlem74  46424  fourierdlem75  46425  fourierdlem102  46452  fourierdlem103  46453  fourierdlem104  46454  fourierdlem114  46464  sge0split  46653  elhoi  46786  mbfresmf  46983  cjnpoly  47135  cfsetsnfsetf1  47305  cfsetsnfsetfo  47306  focofob  47326  f1ocof1ob  47327  fafvelcdm  47416  ffnafv  47417  fafv2elcdm  47480  fafv2elrnb  47481  imarnf1pr  47528  2ffzoeq  47573  fundcmpsurbijinjpreimafv  47653  fundcmpsurinjimaid  47657  fargshiftfv  47685  fargshiftf  47686  fargshiftf1  47687  fargshiftfo  47688  cycl3grtri  48193  fdmdifeqresdif  48588  fdivmpt  48786  fdivmptf  48787  refdivmptf  48788  1arymaptf1  48888  2arymaptf1  48899  ackfnnn0  48931  homf0  49254  aacllem  50046