Theorem ffn 6659

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

Syntax hints:   → wi 4   ⊆ wss 3898  ran crn 5622   Fn wfn 6484  ⟶wf 6485

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 6493

This theorem is referenced by:  ffnd  6660  ffun  6662  frel  6664  fdm  6668  ffrn  6672  fresin  6700  fresaun  6702  fresaunres2  6703  fcoi1  6705  feu  6707  f0bi  6714  dffo2  6747  fimadmfo  6752  fdmeu  6887  feqmptdf  6901  fimarab  6905  fvco3  6930  ffvelcdm  7023  dff2  7041  dffo3  7044  dffo4  7045  dffo5  7046  dffo3f  7048  f1ompt  7053  ffnfv  7061  fcdmssb  7064  fcompt  7075  fsn2  7078  fprb  7137  fconst2g  7146  fpr2g  7154  fex  7169  dff13  7197  nvocnv  7224  soisores  7270  fdmexb  7846  resf1extb  7873  fo1stres  7956  fo2ndres  7957  1stcof  7960  2ndcof  7961  curry1f  8045  curry2f  8047  fparlem1  8051  fparlem2  8052  fo2ndf  8060  soseq  8098  tposf2  8189  smo11  8293  fsetexb  8797  mapsnd  8820  pw2f1olem  9005  mapen  9065  mapunen  9070  fissuni  9252  fipreima  9253  indexfi  9255  mapfien  9303  oismo  9437  cantnflt  9573  cantnfp1lem3  9581  cantnflem4  9593  tcrank  9788  updjudhcoinlf  9836  updjudhcoinrg  9837  updjud  9838  infpwfien  9964  cardinfima  9999  dfacacn  10044  cfflb  10161  cofsmo  10171  cfcoflem  10174  coftr  10175  fin23lem40  10253  axdc3lem2  10353  ac6num  10381  ac6c4  10383  ac6s2  10388  ttukeylem6  10416  iunfo  10441  pwcfsdom  10485  fpwwe2lem5  10537  fpwwe2lem7  10539  pwfseqlem3  10562  inar1  10677  tskcard  10683  tskuni  10685  tskurn  10691  gruima  10704  nqerrel  10834  recmulnq  10866  dmrecnq  10870  axpre-sup  11071  ofsubeq0  12133  dfz2  12498  uzn0  12759  rpnnen1lem3  12883  rpnnen1lem5  12885  unirnioo  13356  dfioo2  13357  ioorebas  13358  fseq1p1m1  13505  2ffzeq  13556  fvinim0ffz  13696  injresinjlem  13697  fsequb2  13890  fseqsupcl  13891  fseqsupubi  13892  ser0f  13969  hashgval  14247  hashinf  14249  hashresfn  14254  ffz0hash  14361  fnfzo0hash  14364  wrdred1hash  14475  revlen  14676  revrev  14681  repswlen  14690  repsdf2  14692  cshword  14705  0csh0  14707  lenco  14746  s1co  14747  cshco  14750  swrdco  14751  s7f1o  14880  ofccat  14883  shftf  14993  uzin2  15259  rexanuz  15260  limsuple  15392  limsupval2  15394  rlimres  15472  lo1res  15473  rlimresb  15479  isercolllem2  15580  isercolllem3  15581  isercoll  15582  supcvg  15770  prodf1f  15806  eff2  16015  reeff1  16036  tanval  16044  ruclem4  16150  ruclem12  16157  prmreclem6  16840  1arithlem4  16845  1arith  16846  vdwmc  16897  vdwlem1  16900  vdwlem8  16907  vdwlem13  16912  ramval  16927  0ram  16939  0ram2  16940  0ramcl  16942  ramcl  16948  fsets  17087  firest  17343  0ssc  17752  0subcat  17753  isfull2  17828  arwhoma  17960  gsumval2a  18601  isgrpinv  18914  kerf1ghm  19167  f1omvdconj  19366  pmtrmvd  19376  pmtrfinv  19381  pmtrdifellem4  19399  efgsfo  19659  efgredlem  19667  efgcpbllemb  19675  frgpup3lem  19697  0frgp  19699  gexex  19773  torsubg  19774  gsumval3  19827  gsumzres  19829  gsummptmhm  19860  gsumzoppg  19864  dprdf1o  19954  dprd2db  19965  zrinitorngc  20566  zrtermorngc  20567  zrtermoringc  20599  srngf1o  20772  lmhmima  20990  lmhmpreima  20991  lmhmrnlss  20993  lspextmo  20999  pwssplit1  21002  cnfldadd  21306  cnfldmul  21308  dfcnfldOLD  21316  cnfldplusf  21342  cnfldsub  21343  chrrhm  21477  znunit  21509  psgnevpmb  21533  psgndiflemB  21546  mpofrlmd  21723  frlmipval  21725  frlmphl  21727  frlmlbs  21743  frlmup4  21747  ellspd  21748  lindfmm  21773  lsslindf  21776  psrbaglefi  21873  psrlidm  21908  mplmonmul  21982  evlseu  22029  mpfconst  22055  mpfproj  22056  mpfsubrg  22057  coe1sclmulfv  22216  pf1const  22281  pf1id  22282  pf1subrg  22283  mpfpf1  22286  pf1mpf  22287  mamuass  22337  mamudi  22338  mamudir  22339  mamuvs1  22340  mamuvs2  22341  1mavmul  22483  mavmulass  22484  mdetunilem7  22553  madutpos  22577  lecldbas  23154  lmbr2  23194  cncnpi  23213  cncnp  23215  cnpdis  23228  lmff  23236  pnrmopn  23278  dnsconst  23313  cmpsub  23335  tgcmp  23336  hauscmplem  23341  2ndcctbss  23390  2ndcomap  23393  2ndcsep  23394  1stccnp  23397  kgenidm  23482  iskgen2  23483  1stckgen  23489  kgen2cn  23494  ptpjpre1  23506  pttop  23517  ptuni  23529  ptval2  23536  tx1cn  23544  tx2cn  23545  ptpjcn  23546  ptpjopn  23547  ptclsg  23550  ptcnplem  23556  upxp  23558  txcnmpt  23559  uptx  23560  txcmplem2  23577  txkgen  23587  xkoptsub  23589  xkopt  23590  xkococnlem  23594  xkococn  23595  ptcmpfi  23748  zfbas  23831  uzrest  23832  rnelfmlem  23887  rnelfm  23888  fmfnfmlem2  23890  fmfnfm  23893  lmflf  23940  alexsubALT  23986  clssubg  24044  qustgplem  24056  tsmsres  24079  tsmsxplem1  24088  ucncn  24219  xmettpos  24284  imasdsf1olem  24308  blrnps  24343  blrn  24344  xmeterval  24367  tmslem  24417  tmsxms  24421  imasf1oxms  24424  prdsxms  24465  blval2  24497  metuel2  24500  isngp2  24532  isngp3  24533  tngngp2  24587  isnghm  24658  qtopbaslem  24693  qdensere  24704  cnbl0  24708  cnblcld  24709  cnfldms  24710  blssioo  24730  tgioo  24731  tgqioo  24735  xrtgioo  24742  xrsdsre  24746  xrge0tsms  24770  iimulcnOLD  24882  bndth  24904  lebnumlem3  24909  nmhmcn  25067  cphsqrtcl  25131  lmmbr2  25206  caucfil  25230  causs  25245  lmcau  25260  bcth3  25278  cncms  25302  cnfldcusp  25304  rrxmvallem  25351  ivthicc  25406  ovolfioo  25415  ovolficc  25416  ovolficcss  25417  ovollb2lem  25436  ovoliunlem2  25451  ovolshftlem1  25457  ovolicc2  25470  ismbl  25474  voliunlem2  25499  volsup  25504  ioorf  25521  ioorinv  25524  ioorcl  25525  uniiccdif  25526  uniioovol  25527  uniiccvol  25528  uniioombllem2  25531  uniioombllem4  25534  dyaddisj  25544  dyadmax  25546  dyadmbllem  25547  dyadmbl  25548  opnmbllem  25549  opnmblALT  25551  volsup2  25553  mbfdm  25574  mbfima  25578  mbfid  25583  ismbfd  25587  mbfres2  25593  mbfposr  25600  mbfimaopnlem  25603  mbflimsup  25614  0plef  25620  i1f1lem  25637  itg11  25639  itg1addlem4  25647  i1fpos  25654  itg1le  25661  itg1climres  25662  mbfi1fseqlem5  25667  mbfi1flimlem  25670  xrge0f  25679  itg2ge0  25683  itg2seq  25690  itg2i1fseqle  25702  itg2i1fseq2  25704  itg2addlem  25706  itg2gt0  25708  limciun  25842  dvres  25859  dvres3a  25862  cpnres  25886  dvfre  25902  dvmptres3  25907  dvlip2  25947  dvgt0lem2  25955  deg1fvi  26037  uc1pmon1p  26104  fta1g  26122  ig1peu  26127  ig1pdvds  26132  plyco0  26144  plypf1  26164  dgrlem  26181  dgrub  26186  dgrlb  26188  coemulc  26207  plyreres  26237  plydivlem3  26250  plydivlem4  26251  plydiveu  26253  plyremlem  26259  fta1lem  26262  fta1  26263  vieta1lem2  26266  plyexmo  26268  elaa  26271  elqaalem3  26276  aannenlem1  26283  pserulm  26378  psercnlem2  26381  psercnlem1  26382  psercn  26383  abelth  26398  reeff1o  26404  pilem1  26408  recosf1o  26491  resinf1o  26492  efif1olem3  26500  efif1olem4  26501  efifo  26503  eff1olem  26504  ellogrn  26515  logcn  26603  dvloglem  26604  logf1o2  26606  efopnlem1  26612  efopnlem2  26613  efopn  26614  logtayl  26616  cxpcn3lem  26704  cxpcn3  26705  resqrtcn  26706  asinneg  26843  areambl  26915  emcllem7  26959  lgamgulm2  26993  basellem4  27041  sqff1o  27139  mpodvdsmulf1o  27151  fsumdvdsmul  27152  dvdsmulf1o  27153  fsumdvdsmulOLD  27154  ostthlem1  27585  ostth  27597  noetasuplem4  27695  madeval2  27814  elold  27834  old1  27840  madeoldsuc  27850  tglnfn  28545  f1otrg  28869  axlowdimlem6  28946  axlowdimlem8  28948  axlowdimlem9  28949  axlowdimlem11  28951  axlowdimlem12  28952  axlowdimlem17  28957  elntg2  28984  dfpth2  29728  cyclnumvtx  29799  crctcshlem4  29819  clwlkclwwlklem2  30001  eucrct2eupth  30246  ex-fpar  30463  cnnvm  30683  sspmlem  30733  nvo00  30762  nmlno0lem  30794  phoeqi  30858  ubthlem1  30871  hhip  31178  hhssabloilem  31262  hhssnv  31265  hhsssh  31270  occllem  31304  shsel  31315  chscllem2  31639  df0op2  31753  hoeq  31761  hocofni  31768  hoaddfni  31771  hosubfni  31772  hon0  31794  ho01i  31829  hoeq1  31831  elnlfn  31929  nmlnop0iALT  31996  lnopco0i  32005  imaelshi  32059  nlelchi  32062  rnbra  32108  cnvbraval  32111  kbass5  32121  hmopidmchi  32152  hmopidmpji  32153  foresf1o  32505  fcomptf  32662  ofpreima  32669  resf1o  32737  maprnin  32738  fpwrelmapffslem  32739  hashgt1  32816  indpi1  32869  indpreima  32875  s3clhash  32958  gsumpart  33074  xrge0tsmsd  33083  tocyc01  33128  cyc3evpm  33160  cycpmgcl  33163  cycpmconjslem2  33165  cyc3conja  33167  kerunit  33334  1arithidomlem1  33544  1arithidomlem2  33545  1arithidom  33546  dimval  33685  dimvalfi  33686  ply1degltdimlem  33707  ply1degltdim  33708  elirng  33771  txomap  33919  locfinreflem  33925  hauseqcn  33983  xpinpreima  33991  xpinpreima2  33992  tpr2rico  33997  mndpluscn  34011  raddcn  34014  xrge0pluscn  34025  xrge0tmdALT  34031  rge0scvg  34034  pl1cn  34040  elzrhunit  34062  qqhf  34071  cnrrext  34095  qqhre  34105  1stmbfm  34345  2ndmbfm  34346  mbfmcnt  34353  omssubadd  34385  carsggect  34403  eulerpartlemsv2  34443  eulerpartlems  34445  eulerpartlemv  34449  eulerpartlemb  34453  eulerpartlemf  34455  eulerpartlemt  34456  eulerpartlemmf  34460  eulerpartlemgvv  34461  eulerpartlemgh  34463  eulerpartlemgs2  34465  sseqmw  34476  sseqf  34477  sseqp1  34480  fiblem  34483  fibp1  34486  plymul02  34631  signsvtn0  34655  signstres  34660  signshlen  34675  reprinrn  34703  circlemethhgt  34728  txsconnlem  35356  iccllysconn  35366  rellysconn  35367  cvmseu  35392  cvmliftmolem2  35398  cvmliftlem6  35406  cvmliftlem7  35407  cvmliftlem8  35408  cvmliftlem9  35409  cvmliftlem11  35411  cvmliftlem15  35414  cvmlift2lem7  35425  cvmlift2lem10  35428  cvmlift3lem8  35442  cvmlift3lem9  35443  mvrsfpw  35622  mrsubff1  35630  msrid  35661  msrfo  35662  elmsta  35664  mtyf  35668  msubff1  35672  vhmcls  35682  mclsax  35685  elmthm  35692  mthmblem  35696  mclsppslem  35699  iprodefisumlem  35856  fullfunfnv  36062  fullfunfv  36063  tailfb  36493  filnetlem4  36497  taupilem3  37436  icoreresf  37469  icoreelrnab  37471  relowlssretop  37480  relowlpssretop  37481  unccur  37716  matunitlindflem1  37729  matunitlindflem2  37730  ptrecube  37733  poimirlem28  37761  poimirlem32  37765  heicant  37768  opnmbllem0  37769  mblfinlem1  37770  mblfinlem2  37771  volsupnfl  37778  cnambfre  37781  dvtan  37783  itg2addnclem  37784  itg2addnclem2  37785  ftc1anclem3  37808  ftc1anclem5  37810  ftc1anclem7  37812  ftc1anclem8  37813  ftc1anc  37814  areacirc  37826  indexdom  37847  sdclem2  37855  sstotbnd2  37887  sstotbnd  37888  isbndx  37895  isbnd3b  37898  prdsbnd  37906  prdstotbnd  37907  ismtyhmeolem  37917  heibor1lem  37922  heiborlem1  37924  heibor  37934  rrnequiv  37948  keridl  38145  ellkr  39261  lkr0f  39266  cdleme50rnlem  40716  aks6d1c2lem4  42293  aks6d1c5  42305  sticksstones11  42322  sticksstones19  42331  sticksstones22  42334  aks6d1c6lem4  42339  aks6d1c6isolem2  42341  fsuppind  42748  elrfirn  42852  ismrcd2  42856  isnacs2  42863  nacsfix  42869  mapfzcons1  42874  mzpcompact2lem  42908  eq0rabdioph  42933  eldioph4b  42968  diophren  42970  pw2f1ocnv  43194  pw2f1o2val2  43197  lmhmfgsplit  43243  pwssplit4  43246  hbt  43287  mpaaeu  43307  mendring  43345  proot1mul  43351  proot1hash  43352  proot1ex  43353  deg1mhm  43357  fgraphopab  43360  hausgraph  43362  nvocnvb  43579  ofsubid  44481  expgrowthi  44490  expgrowth  44492  binomcxplemdvbinom  44510  binomcxplemcvg  44511  binomcxplemnotnn0  44513  relpfrlem  45110  rfcnpre1  45180  rfcnpre2  45192  cncmpmax  45193  rfcnpre3  45194  rfcnpre4  45195  elixpconstg  45249  ffi  45333  islptre  45781  resincncf  46035  dvcosre  46072  dvresntr  46078  volioof  46147  stoweidlem48  46208  fourierdlem12  46279  fourierdlem15  46282  fourierdlem41  46308  fourierdlem42  46309  fourierdlem46  46312  fourierdlem48  46314  fourierdlem49  46315  fourierdlem54  46320  fourierdlem56  46322  fourierdlem62  46328  fourierdlem64  46330  fourierdlem65  46331  fourierdlem73  46339  fourierdlem74  46340  fourierdlem75  46341  fourierdlem102  46368  fourierdlem103  46369  fourierdlem104  46370  fourierdlem114  46380  sge0split  46569  elhoi  46702  mbfresmf  46899  cjnpoly  47051  cfsetsnfsetf1  47221  cfsetsnfsetfo  47222  focofob  47242  f1ocof1ob  47243  fafvelcdm  47332  ffnafv  47333  fafv2elcdm  47396  fafv2elrnb  47397  imarnf1pr  47444  2ffzoeq  47489  fundcmpsurbijinjpreimafv  47569  fundcmpsurinjimaid  47573  fargshiftfv  47601  fargshiftf  47602  fargshiftf1  47603  fargshiftfo  47604  cycl3grtri  48109  fdmdifeqresdif  48504  fdivmpt  48702  fdivmptf  48703  refdivmptf  48704  1arymaptf1  48804  2arymaptf1  48815  ackfnnn0  48847  homf0  49170  aacllem  49962