Theorem ffn 6655

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 6489	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2	1	simplbi 497	1 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   ⊆ wss 3883  ran crn 5619   Fn wfn 6480  ⟶wf 6481

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 208  df-an 397  df-f 6489

This theorem is referenced by:  ffnd  6656  ffun  6658  frel  6660  fdm  6664  ffrn  6668  fresin  6696  fresaun  6698  fresaunres2  6699  fcoi1  6701  feu  6703  f0bi  6710  dffo2  6743  fimadmfo  6748  fdmeu  6883  feqmptdf  6897  fimarab  6901  fvco3  6927  ffvelcdm  7022  dff2  7040  dffo3  7043  dffo4  7044  dffo5  7045  dffo3f  7047  f1ompt  7052  ffnfv  7060  fcdmssb  7063  fcompt  7075  fsn2  7078  fprb  7138  fconst2g  7147  fpr2g  7155  fex  7170  dff13  7198  nvocnv  7225  soisores  7271  fdmexb  7847  resf1extb  7874  fo1stres  7957  fo2ndres  7958  1stcof  7961  2ndcof  7962  curry1f  8045  curry2f  8047  fparlem1  8051  fparlem2  8052  fo2ndf  8060  soseq  8099  tposf2  8190  smo11  8294  fsetexb  8801  mapsnd  8824  pw2f1olem  9009  mapen  9069  mapunen  9074  fissuni  9257  fipreima  9258  indexfi  9260  mapfien  9311  oismo  9445  cantnflt  9584  cantnfp1lem3  9592  cantnflem4  9604  tcrank  9799  updjudhcoinlf  9847  updjudhcoinrg  9848  updjud  9849  infpwfien  9975  cardinfima  10010  dfacacn  10055  cfflb  10172  cofsmo  10182  cfcoflem  10185  coftr  10186  fin23lem40  10264  axdc3lem2  10364  ac6num  10392  ac6c4  10394  ac6s2  10399  ttukeylem6  10427  iunfo  10452  pwcfsdom  10497  fpwwe2lem5  10549  fpwwe2lem7  10551  pwfseqlem3  10574  inar1  10689  tskcard  10695  tskuni  10697  tskurn  10703  gruima  10716  nqerrel  10846  recmulnq  10878  dmrecnq  10882  axpre-sup  11083  ofsubeq0  12147  indpi1  12164  dfz2  12534  uzn0  12796  rpnnen1lem3  12920  rpnnen1lem5  12922  unirnioo  13393  dfioo2  13394  ioorebas  13395  fseq1p1m1  13543  2ffzeq  13594  fvinim0ffz  13735  injresinjlem  13736  fsequb2  13929  fseqsupcl  13930  fseqsupubi  13931  ser0f  14008  hashgval  14286  hashinf  14288  hashresfn  14293  ffz0hash  14400  fnfzo0hash  14403  wrdred1hash  14514  revlen  14715  revrev  14720  repswlen  14729  repsdf2  14731  cshword  14744  0csh0  14746  lenco  14785  s1co  14786  cshco  14789  swrdco  14790  s7f1o  14919  ofccat  14922  shftf  15032  uzin2  15298  rexanuz  15299  limsuple  15431  limsupval2  15433  rlimres  15511  lo1res  15512  rlimresb  15518  isercolllem2  15619  isercolllem3  15620  isercoll  15621  supcvg  15812  prodf1f  15848  eff2  16057  reeff1  16078  tanval  16086  ruclem4  16192  ruclem12  16199  prmreclem6  16883  1arithlem4  16888  1arith  16889  vdwmc  16940  vdwlem1  16943  vdwlem8  16950  vdwlem13  16955  ramval  16970  0ram  16982  0ram2  16983  0ramcl  16985  ramcl  16991  fsets  17130  firest  17386  0ssc  17795  0subcat  17796  isfull2  17871  arwhoma  18003  gsumval2a  18644  isgrpinv  18960  kerf1ghm  19213  f1omvdconj  19412  pmtrmvd  19422  pmtrfinv  19427  pmtrdifellem4  19445  efgsfo  19705  efgredlem  19713  efgcpbllemb  19721  frgpup3lem  19743  0frgp  19745  gexex  19819  torsubg  19820  gsumval3  19873  gsumzres  19875  gsummptmhm  19906  gsumzoppg  19910  dprdf1o  20000  dprd2db  20011  zrinitorngc  20614  zrtermorngc  20615  zrtermoringc  20647  srngf1o  20820  lmhmima  21037  lmhmpreima  21038  lmhmrnlss  21040  lspextmo  21046  pwssplit1  21049  cnfldadd  21353  cnfldmul  21355  cnfldplusf  21374  cnfldsub  21375  chrrhm  21506  znunit  21538  psgnevpmb  21562  psgndiflemB  21575  mpofrlmd  21752  frlmipval  21754  frlmphl  21756  frlmlbs  21772  frlmup4  21776  ellspd  21777  lindfmm  21802  lsslindf  21805  psrbaglefi  21901  psrlidm  21936  mplmonmul  22012  evlseu  22059  mpfconst  22085  mpfproj  22086  mpfsubrg  22087  coe1sclmulfv  22269  pf1const  22332  pf1id  22333  pf1subrg  22334  mpfpf1  22337  pf1mpf  22338  mamuass  22385  mamudi  22386  mamudir  22387  mamuvs1  22388  mamuvs2  22389  1mavmul  22531  mavmulass  22532  mdetunilem7  22601  madutpos  22625  lecldbas  23202  lmbr2  23242  cncnpi  23261  cncnp  23263  cnpdis  23276  lmff  23284  pnrmopn  23326  dnsconst  23361  cmpsub  23383  tgcmp  23384  hauscmplem  23389  2ndcctbss  23438  2ndcomap  23441  2ndcsep  23442  1stccnp  23445  kgenidm  23530  iskgen2  23531  1stckgen  23537  kgen2cn  23542  ptpjpre1  23554  pttop  23565  ptuni  23577  ptval2  23584  tx1cn  23592  tx2cn  23593  ptpjcn  23594  ptpjopn  23595  ptclsg  23598  ptcnplem  23604  upxp  23606  txcnmpt  23607  uptx  23608  txcmplem2  23625  txkgen  23635  xkoptsub  23637  xkopt  23638  xkococnlem  23642  xkococn  23643  ptcmpfi  23796  zfbas  23879  uzrest  23880  rnelfmlem  23935  rnelfm  23936  fmfnfmlem2  23938  fmfnfm  23941  lmflf  23988  alexsubALT  24034  clssubg  24092  qustgplem  24104  tsmsres  24127  tsmsxplem1  24136  ucncn  24267  xmettpos  24332  imasdsf1olem  24356  blrnps  24391  blrn  24392  xmeterval  24415  tmslem  24465  tmsxms  24469  imasf1oxms  24472  prdsxms  24513  blval2  24545  metuel2  24548  isngp2  24580  isngp3  24581  tngngp2  24635  isnghm  24706  qtopbaslem  24741  qdensere  24752  cnbl0  24756  cnblcld  24757  cnfldms  24758  blssioo  24778  tgioo  24779  tgqioo  24783  xrtgioo  24790  xrsdsre  24794  xrge0tsms  24818  bndth  24943  lebnumlem3  24948  nmhmcn  25105  cphsqrtcl  25169  lmmbr2  25244  caucfil  25268  causs  25283  lmcau  25298  bcth3  25316  cncms  25340  cnfldcusp  25342  rrxmvallem  25389  ivthicc  25443  ovolfioo  25452  ovolficc  25453  ovolficcss  25454  ovollb2lem  25473  ovoliunlem2  25488  ovolshftlem1  25494  ovolicc2  25507  ismbl  25511  voliunlem2  25536  volsup  25541  ioorf  25558  ioorinv  25561  ioorcl  25562  uniiccdif  25563  uniioovol  25564  uniiccvol  25565  uniioombllem2  25568  uniioombllem4  25571  dyaddisj  25581  dyadmax  25583  dyadmbllem  25584  dyadmbl  25585  opnmbllem  25586  opnmblALT  25588  volsup2  25590  mbfdm  25611  mbfima  25615  mbfid  25620  ismbfd  25624  mbfres2  25630  mbfposr  25637  mbfimaopnlem  25640  mbflimsup  25651  0plef  25657  i1f1lem  25674  itg11  25676  itg1addlem4  25684  i1fpos  25691  itg1le  25698  itg1climres  25699  mbfi1fseqlem5  25704  mbfi1flimlem  25707  xrge0f  25716  itg2ge0  25720  itg2seq  25727  itg2i1fseqle  25739  itg2i1fseq2  25741  itg2addlem  25743  itg2gt0  25745  limciun  25879  dvres  25896  dvres3a  25899  cpnres  25922  dvfre  25936  dvmptres3  25941  dvlip2  25980  dvgt0lem2  25988  deg1fvi  26068  uc1pmon1p  26135  fta1g  26153  ig1peu  26158  ig1pdvds  26163  plyco0  26175  plypf1  26195  dgrlem  26212  dgrub  26217  dgrlb  26219  coemulc  26238  plyreres  26267  plydivlem3  26279  plydivlem4  26280  plydiveu  26282  plyremlem  26288  fta1lem  26291  fta1  26292  vieta1lem2  26295  plyexmo  26297  elaa  26300  elqaalem3  26305  aannenlem1  26312  pserulm  26405  psercnlem2  26407  psercnlem1  26408  psercn  26409  abelth  26424  reeff1o  26430  pilem1  26434  recosf1o  26517  resinf1o  26518  efif1olem3  26526  efif1olem4  26527  efifo  26529  eff1olem  26530  ellogrn  26541  logcn  26629  dvloglem  26630  logf1o2  26632  efopnlem1  26638  efopnlem2  26639  efopn  26640  logtayl  26642  cxpcn3lem  26729  cxpcn3  26730  resqrtcn  26731  asinneg  26868  areambl  26940  emcllem7  26983  lgamgulm2  27017  basellem4  27065  sqff1o  27163  mpodvdsmulf1o  27175  fsumdvdsmul  27176  dvdsmulf1o  27177  ostthlem1  27608  ostth  27620  noetasuplem4  27718  madeval2  27843  elold  27869  old1  27875  madeoldsuc  27895  tglnfn  28633  f1otrg  28957  axlowdimlem6  29034  axlowdimlem8  29036  axlowdimlem9  29037  axlowdimlem11  29039  axlowdimlem12  29040  axlowdimlem17  29045  elntg2  29072  dfpth2  29815  cyclnumvtx  29886  crctcshlem4  29906  clwlkclwwlklem2  30088  eucrct2eupth  30333  ex-fpar  30550  cnnvm  30771  sspmlem  30821  nvo00  30850  nmlno0lem  30882  phoeqi  30946  ubthlem1  30959  hhip  31266  hhssabloilem  31350  hhssnv  31353  hhsssh  31358  occllem  31392  shsel  31403  chscllem2  31727  df0op2  31841  hoeq  31849  hocofni  31856  hoaddfni  31859  hosubfni  31860  hon0  31882  ho01i  31917  hoeq1  31919  elnlfn  32017  nmlnop0iALT  32084  lnopco0i  32093  imaelshi  32147  nlelchi  32150  rnbra  32196  cnvbraval  32199  kbass5  32209  hmopidmchi  32240  hmopidmpji  32241  foresf1o  32592  fcomptf  32750  ofpreima  32757  resf1o  32822  maprnin  32823  fpwrelmapffslem  32824  hashgt1  32900  indpreima  32944  s3clhash  33027  gsumpart  33144  xrge0tsmsd  33154  tocyc01  33199  cyc3evpm  33231  cycpmgcl  33234  cycpmconjslem2  33236  cyc3conja  33238  kerunit  33408  1arithidomlem1  33618  1arithidomlem2  33619  1arithidom  33620  psrmonmul  33734  dimval  33785  dimvalfi  33786  ply1degltdimlem  33806  ply1degltdim  33807  elirng  33870  txomap  34018  locfinreflem  34024  hauseqcn  34082  xpinpreima  34090  xpinpreima2  34091  tpr2rico  34096  mndpluscn  34110  raddcn  34113  xrge0pluscn  34124  xrge0tmdALT  34130  rge0scvg  34133  pl1cn  34139  elzrhunit  34161  qqhf  34170  cnrrext  34194  qqhre  34204  1stmbfm  34444  2ndmbfm  34445  mbfmcnt  34452  omssubadd  34484  carsggect  34502  eulerpartlemsv2  34542  eulerpartlems  34544  eulerpartlemv  34548  eulerpartlemb  34552  eulerpartlemf  34554  eulerpartlemt  34555  eulerpartlemmf  34559  eulerpartlemgvv  34560  eulerpartlemgh  34562  eulerpartlemgs2  34564  sseqmw  34575  sseqf  34576  sseqp1  34579  fiblem  34582  fibp1  34585  plymul02  34730  signsvtn0  34754  signstres  34759  signshlen  34774  reprinrn  34802  circlemethhgt  34827  txsconnlem  35468  iccllysconn  35478  rellysconn  35479  cvmseu  35504  cvmliftmolem2  35510  cvmliftlem6  35518  cvmliftlem7  35519  cvmliftlem8  35520  cvmliftlem9  35521  cvmliftlem11  35523  cvmliftlem15  35526  cvmlift2lem7  35537  cvmlift2lem10  35540  cvmlift3lem8  35554  cvmlift3lem9  35555  mvrsfpw  35734  mrsubff1  35742  msrid  35773  msrfo  35774  elmsta  35776  mtyf  35780  msubff1  35784  vhmcls  35794  mclsax  35797  elmthm  35804  mthmblem  35808  mclsppslem  35811  iprodefisumlem  35968  fullfunfnv  36174  fullfunfv  36175  tailfb  36605  filnetlem4  36609  regsfromunir1  36768  taupilem3  37679  icoreresf  37714  icoreelrnab  37716  relowlssretop  37725  relowlpssretop  37726  unccur  37970  matunitlindflem1  37983  matunitlindflem2  37984  ptrecube  37987  poimirlem28  38015  poimirlem32  38019  heicant  38022  opnmbllem0  38023  mblfinlem1  38024  mblfinlem2  38025  volsupnfl  38032  cnambfre  38035  dvtan  38037  itg2addnclem  38038  itg2addnclem2  38039  ftc1anclem3  38062  ftc1anclem5  38064  ftc1anclem7  38066  ftc1anclem8  38067  ftc1anc  38068  areacirc  38080  indexdom  38101  sdclem2  38109  sstotbnd2  38141  sstotbnd  38142  isbndx  38149  isbnd3b  38152  prdsbnd  38160  prdstotbnd  38161  ismtyhmeolem  38171  heibor1lem  38176  heiborlem1  38178  heibor  38188  rrnequiv  38202  keridl  38399  ellkr  39581  lkr0f  39586  cdleme50rnlem  41036  aks6d1c2lem4  42612  aks6d1c5  42624  sticksstones11  42641  sticksstones19  42650  sticksstones22  42653  aks6d1c6lem4  42658  aks6d1c6isolem2  42660  fsuppind  43040  elrfirn  43144  ismrcd2  43148  isnacs2  43155  nacsfix  43161  mapfzcons1  43166  mzpcompact2lem  43200  eq0rabdioph  43225  eldioph4b  43256  diophren  43258  pw2f1ocnv  43482  pw2f1o2val2  43485  lmhmfgsplit  43531  pwssplit4  43534  hbt  43575  mpaaeu  43595  mendring  43633  proot1mul  43639  proot1hash  43640  proot1ex  43641  deg1mhm  43645  fgraphopab  43648  hausgraph  43650  nvocnvb  43866  ofsubid  44768  expgrowthi  44777  expgrowth  44779  binomcxplemdvbinom  44797  binomcxplemcvg  44798  binomcxplemnotnn0  44800  relpfrlem  45397  rfcnpre1  45467  rfcnpre2  45479  cncmpmax  45480  rfcnpre3  45481  rfcnpre4  45482  elixpconstg  45536  ffi  45620  islptre  46064  resincncf  46318  dvcosre  46355  dvresntr  46361  volioof  46430  stoweidlem48  46491  fourierdlem12  46562  fourierdlem15  46565  fourierdlem41  46591  fourierdlem42  46592  fourierdlem46  46595  fourierdlem48  46597  fourierdlem49  46598  fourierdlem54  46603  fourierdlem56  46605  fourierdlem62  46611  fourierdlem64  46613  fourierdlem65  46614  fourierdlem73  46622  fourierdlem74  46623  fourierdlem75  46624  fourierdlem102  46651  fourierdlem103  46652  fourierdlem104  46653  fourierdlem114  46663  sge0split  46852  elhoi  46985  mbfresmf  47182  cjnpoly  47352  cfsetsnfsetf1  47522  cfsetsnfsetfo  47523  focofob  47543  f1ocof1ob  47544  fafvelcdm  47633  ffnafv  47634  fafv2elcdm  47697  fafv2elrnb  47698  imarnf1pr  47745  2ffzoeq  47791  fundcmpsurbijinjpreimafv  47882  fundcmpsurinjimaid  47886  fargshiftfv  47914  fargshiftf  47915  fargshiftf1  47916  fargshiftfo  47917  cycl3grtri  48438  fdmdifeqresdif  48833  fdivmpt  49031  fdivmptf  49032  refdivmptf  49033  1arymaptf1  49133  2arymaptf1  49144  ackfnnn0  49176  homf0  49499  aacllem  50291