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 496	1 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   ⊆ wss 3890  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  7027  dff2  7045  dffo3  7048  dffo4  7049  dffo5  7050  dffo3f  7052  f1ompt  7057  ffnfv  7065  fcdmssb  7068  fcompt  7080  fsn2  7083  fprb  7142  fconst2g  7151  fpr2g  7159  fex  7174  dff13  7202  nvocnv  7229  soisores  7275  fdmexb  7851  resf1extb  7878  fo1stres  7961  fo2ndres  7962  1stcof  7965  2ndcof  7966  curry1f  8049  curry2f  8051  fparlem1  8055  fparlem2  8056  fo2ndf  8064  soseq  8102  tposf2  8193  smo11  8297  fsetexb  8804  mapsnd  8827  pw2f1olem  9012  mapen  9072  mapunen  9077  fissuni  9260  fipreima  9261  indexfi  9263  mapfien  9314  oismo  9448  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  20610  zrtermorngc  20611  zrtermoringc  20643  srngf1o  20816  lmhmima  21034  lmhmpreima  21035  lmhmrnlss  21037  lspextmo  21043  pwssplit1  21046  cnfldadd  21350  cnfldmul  21352  dfcnfldOLD  21360  cnfldplusf  21386  cnfldsub  21387  chrrhm  21521  znunit  21553  psgnevpmb  21577  psgndiflemB  21590  mpofrlmd  21767  frlmipval  21769  frlmphl  21771  frlmlbs  21787  frlmup4  21791  ellspd  21792  lindfmm  21817  lsslindf  21820  psrbaglefi  21916  psrlidm  21950  mplmonmul  22024  evlseu  22071  mpfconst  22097  mpfproj  22098  mpfsubrg  22099  coe1sclmulfv  22258  pf1const  22321  pf1id  22322  pf1subrg  22323  mpfpf1  22326  pf1mpf  22327  mamuass  22377  mamudi  22378  mamudir  22379  mamuvs1  22380  mamuvs2  22381  1mavmul  22523  mavmulass  22524  mdetunilem7  22593  madutpos  22617  lecldbas  23194  lmbr2  23234  cncnpi  23253  cncnp  23255  cnpdis  23268  lmff  23276  pnrmopn  23318  dnsconst  23353  cmpsub  23375  tgcmp  23376  hauscmplem  23381  2ndcctbss  23430  2ndcomap  23433  2ndcsep  23434  1stccnp  23437  kgenidm  23522  iskgen2  23523  1stckgen  23529  kgen2cn  23534  ptpjpre1  23546  pttop  23557  ptuni  23569  ptval2  23576  tx1cn  23584  tx2cn  23585  ptpjcn  23586  ptpjopn  23587  ptclsg  23590  ptcnplem  23596  upxp  23598  txcnmpt  23599  uptx  23600  txcmplem2  23617  txkgen  23627  xkoptsub  23629  xkopt  23630  xkococnlem  23634  xkococn  23635  ptcmpfi  23788  zfbas  23871  uzrest  23872  rnelfmlem  23927  rnelfm  23928  fmfnfmlem2  23930  fmfnfm  23933  lmflf  23980  alexsubALT  24026  clssubg  24084  qustgplem  24096  tsmsres  24119  tsmsxplem1  24128  ucncn  24259  xmettpos  24324  imasdsf1olem  24348  blrnps  24383  blrn  24384  xmeterval  24407  tmslem  24457  tmsxms  24461  imasf1oxms  24464  prdsxms  24505  blval2  24537  metuel2  24540  isngp2  24572  isngp3  24573  tngngp2  24627  isnghm  24698  qtopbaslem  24733  qdensere  24744  cnbl0  24748  cnblcld  24749  cnfldms  24750  blssioo  24770  tgioo  24771  tgqioo  24775  xrtgioo  24782  xrsdsre  24786  xrge0tsms  24810  bndth  24935  lebnumlem3  24940  nmhmcn  25097  cphsqrtcl  25161  lmmbr2  25236  caucfil  25260  causs  25275  lmcau  25290  bcth3  25308  cncms  25332  cnfldcusp  25334  rrxmvallem  25381  ivthicc  25435  ovolfioo  25444  ovolficc  25445  ovolficcss  25446  ovollb2lem  25465  ovoliunlem2  25480  ovolshftlem1  25486  ovolicc2  25499  ismbl  25503  voliunlem2  25528  volsup  25533  ioorf  25550  ioorinv  25553  ioorcl  25554  uniiccdif  25555  uniioovol  25556  uniiccvol  25557  uniioombllem2  25560  uniioombllem4  25563  dyaddisj  25573  dyadmax  25575  dyadmbllem  25576  dyadmbl  25577  opnmbllem  25578  opnmblALT  25580  volsup2  25582  mbfdm  25603  mbfima  25607  mbfid  25612  ismbfd  25616  mbfres2  25622  mbfposr  25629  mbfimaopnlem  25632  mbflimsup  25643  0plef  25649  i1f1lem  25666  itg11  25668  itg1addlem4  25676  i1fpos  25683  itg1le  25690  itg1climres  25691  mbfi1fseqlem5  25696  mbfi1flimlem  25699  xrge0f  25708  itg2ge0  25712  itg2seq  25719  itg2i1fseqle  25731  itg2i1fseq2  25733  itg2addlem  25735  itg2gt0  25737  limciun  25871  dvres  25888  dvres3a  25891  cpnres  25914  dvfre  25928  dvmptres3  25933  dvlip2  25972  dvgt0lem2  25980  deg1fvi  26060  uc1pmon1p  26127  fta1g  26145  ig1peu  26150  ig1pdvds  26155  plyco0  26167  plypf1  26187  dgrlem  26204  dgrub  26209  dgrlb  26211  coemulc  26230  plyreres  26259  plydivlem3  26272  plydivlem4  26273  plydiveu  26275  plyremlem  26281  fta1lem  26284  fta1  26285  vieta1lem2  26288  plyexmo  26290  elaa  26293  elqaalem3  26298  aannenlem1  26305  pserulm  26400  psercnlem2  26402  psercnlem1  26403  psercn  26404  abelth  26419  reeff1o  26425  pilem1  26429  recosf1o  26512  resinf1o  26513  efif1olem3  26521  efif1olem4  26522  efifo  26524  eff1olem  26525  ellogrn  26536  logcn  26624  dvloglem  26625  logf1o2  26627  efopnlem1  26633  efopnlem2  26634  efopn  26635  logtayl  26637  cxpcn3lem  26724  cxpcn3  26725  resqrtcn  26726  asinneg  26863  areambl  26935  emcllem7  26979  lgamgulm2  27013  basellem4  27061  sqff1o  27159  mpodvdsmulf1o  27171  fsumdvdsmul  27172  dvdsmulf1o  27173  ostthlem1  27604  ostth  27616  noetasuplem4  27714  madeval2  27839  elold  27865  old1  27871  madeoldsuc  27891  tglnfn  28629  f1otrg  28953  axlowdimlem6  29030  axlowdimlem8  29032  axlowdimlem9  29033  axlowdimlem11  29035  axlowdimlem12  29036  axlowdimlem17  29041  elntg2  29068  dfpth2  29812  cyclnumvtx  29883  crctcshlem4  29903  clwlkclwwlklem2  30085  eucrct2eupth  30330  ex-fpar  30547  cnnvm  30768  sspmlem  30818  nvo00  30847  nmlno0lem  30879  phoeqi  30943  ubthlem1  30956  hhip  31263  hhssabloilem  31347  hhssnv  31350  hhsssh  31355  occllem  31389  shsel  31400  chscllem2  31724  df0op2  31838  hoeq  31846  hocofni  31853  hoaddfni  31856  hosubfni  31857  hon0  31879  ho01i  31914  hoeq1  31916  elnlfn  32014  nmlnop0iALT  32081  lnopco0i  32090  imaelshi  32144  nlelchi  32147  rnbra  32193  cnvbraval  32196  kbass5  32206  hmopidmchi  32237  hmopidmpji  32238  foresf1o  32589  fcomptf  32746  ofpreima  32753  resf1o  32818  maprnin  32819  fpwrelmapffslem  32820  hashgt1  32896  indpreima  32940  s3clhash  33023  gsumpart  33139  xrge0tsmsd  33149  tocyc01  33194  cyc3evpm  33226  cycpmgcl  33229  cycpmconjslem2  33231  cyc3conja  33233  kerunit  33400  1arithidomlem1  33610  1arithidomlem2  33611  1arithidom  33612  psrmonmul  33709  dimval  33760  dimvalfi  33761  ply1degltdimlem  33782  ply1degltdim  33783  elirng  33846  txomap  33994  locfinreflem  34000  hauseqcn  34058  xpinpreima  34066  xpinpreima2  34067  tpr2rico  34072  mndpluscn  34086  raddcn  34089  xrge0pluscn  34100  xrge0tmdALT  34106  rge0scvg  34109  pl1cn  34115  elzrhunit  34137  qqhf  34146  cnrrext  34170  qqhre  34180  1stmbfm  34420  2ndmbfm  34421  mbfmcnt  34428  omssubadd  34460  carsggect  34478  eulerpartlemsv2  34518  eulerpartlems  34520  eulerpartlemv  34524  eulerpartlemb  34528  eulerpartlemf  34530  eulerpartlemt  34531  eulerpartlemmf  34535  eulerpartlemgvv  34536  eulerpartlemgh  34538  eulerpartlemgs2  34540  sseqmw  34551  sseqf  34552  sseqp1  34555  fiblem  34558  fibp1  34561  plymul02  34706  signsvtn0  34730  signstres  34735  signshlen  34750  reprinrn  34778  circlemethhgt  34803  txsconnlem  35438  iccllysconn  35448  rellysconn  35449  cvmseu  35474  cvmliftmolem2  35480  cvmliftlem6  35488  cvmliftlem7  35489  cvmliftlem8  35490  cvmliftlem9  35491  cvmliftlem11  35493  cvmliftlem15  35496  cvmlift2lem7  35507  cvmlift2lem10  35510  cvmlift3lem8  35524  cvmlift3lem9  35525  mvrsfpw  35704  mrsubff1  35712  msrid  35743  msrfo  35744  elmsta  35746  mtyf  35750  msubff1  35754  vhmcls  35764  mclsax  35767  elmthm  35774  mthmblem  35778  mclsppslem  35781  iprodefisumlem  35938  fullfunfnv  36144  fullfunfv  36145  tailfb  36575  filnetlem4  36579  regsfromunir1  36738  taupilem3  37649  icoreresf  37682  icoreelrnab  37684  relowlssretop  37693  relowlpssretop  37694  unccur  37938  matunitlindflem1  37951  matunitlindflem2  37952  ptrecube  37955  poimirlem28  37983  poimirlem32  37987  heicant  37990  opnmbllem0  37991  mblfinlem1  37992  mblfinlem2  37993  volsupnfl  38000  cnambfre  38003  dvtan  38005  itg2addnclem  38006  itg2addnclem2  38007  ftc1anclem3  38030  ftc1anclem5  38032  ftc1anclem7  38034  ftc1anclem8  38035  ftc1anc  38036  areacirc  38048  indexdom  38069  sdclem2  38077  sstotbnd2  38109  sstotbnd  38110  isbndx  38117  isbnd3b  38120  prdsbnd  38128  prdstotbnd  38129  ismtyhmeolem  38139  heibor1lem  38144  heiborlem1  38146  heibor  38156  rrnequiv  38170  keridl  38367  ellkr  39549  lkr0f  39554  cdleme50rnlem  41004  aks6d1c2lem4  42580  aks6d1c5  42592  sticksstones11  42609  sticksstones19  42618  sticksstones22  42621  aks6d1c6lem4  42626  aks6d1c6isolem2  42628  fsuppind  43037  elrfirn  43141  ismrcd2  43145  isnacs2  43152  nacsfix  43158  mapfzcons1  43163  mzpcompact2lem  43197  eq0rabdioph  43222  eldioph4b  43257  diophren  43259  pw2f1ocnv  43483  pw2f1o2val2  43486  lmhmfgsplit  43532  pwssplit4  43535  hbt  43576  mpaaeu  43596  mendring  43634  proot1mul  43640  proot1hash  43641  proot1ex  43642  deg1mhm  43646  fgraphopab  43649  hausgraph  43651  nvocnvb  43867  ofsubid  44769  expgrowthi  44778  expgrowth  44780  binomcxplemdvbinom  44798  binomcxplemcvg  44799  binomcxplemnotnn0  44801  relpfrlem  45398  rfcnpre1  45468  rfcnpre2  45480  cncmpmax  45481  rfcnpre3  45482  rfcnpre4  45483  elixpconstg  45537  ffi  45621  islptre  46067  resincncf  46321  dvcosre  46358  dvresntr  46364  volioof  46433  stoweidlem48  46494  fourierdlem12  46565  fourierdlem15  46568  fourierdlem41  46594  fourierdlem42  46595  fourierdlem46  46598  fourierdlem48  46600  fourierdlem49  46601  fourierdlem54  46606  fourierdlem56  46608  fourierdlem62  46614  fourierdlem64  46616  fourierdlem65  46617  fourierdlem73  46625  fourierdlem74  46626  fourierdlem75  46627  fourierdlem102  46654  fourierdlem103  46655  fourierdlem104  46656  fourierdlem114  46666  sge0split  46855  elhoi  46988  mbfresmf  47185  cjnpoly  47349  cfsetsnfsetf1  47519  cfsetsnfsetfo  47520  focofob  47540  f1ocof1ob  47541  fafvelcdm  47630  ffnafv  47631  fafv2elcdm  47694  fafv2elrnb  47695  imarnf1pr  47742  2ffzoeq  47788  fundcmpsurbijinjpreimafv  47879  fundcmpsurinjimaid  47883  fargshiftfv  47911  fargshiftf  47912  fargshiftf1  47913  fargshiftfo  47914  cycl3grtri  48435  fdmdifeqresdif  48830  fdivmpt  49028  fdivmptf  49029  refdivmptf  49030  1arymaptf1  49130  2arymaptf1  49141  ackfnnn0  49173  homf0  49496  aacllem  50288