Theorem ffn 6670

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

Syntax hints:   → wi 4   ⊆ wss 3903  ran crn 5633   Fn wfn 6495  ⟶wf 6496

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 6504

This theorem is referenced by:  ffnd  6671  ffun  6673  frel  6675  fdm  6679  ffrn  6683  fresin  6711  fresaun  6713  fresaunres2  6714  fcoi1  6716  feu  6718  f0bi  6725  dffo2  6758  fimadmfo  6763  fdmeu  6898  feqmptdf  6912  fimarab  6916  fvco3  6941  ffvelcdm  7035  dff2  7053  dffo3  7056  dffo4  7057  dffo5  7058  dffo3f  7060  f1ompt  7065  ffnfv  7073  fcdmssb  7076  fcompt  7088  fsn2  7091  fprb  7150  fconst2g  7159  fpr2g  7167  fex  7182  dff13  7210  nvocnv  7237  soisores  7283  fdmexb  7859  resf1extb  7886  fo1stres  7969  fo2ndres  7970  1stcof  7973  2ndcof  7974  curry1f  8058  curry2f  8060  fparlem1  8064  fparlem2  8065  fo2ndf  8073  soseq  8111  tposf2  8202  smo11  8306  fsetexb  8813  mapsnd  8836  pw2f1olem  9021  mapen  9081  mapunen  9086  fissuni  9269  fipreima  9270  indexfi  9272  mapfien  9323  oismo  9457  cantnflt  9593  cantnfp1lem3  9601  cantnflem4  9613  tcrank  9808  updjudhcoinlf  9856  updjudhcoinrg  9857  updjud  9858  infpwfien  9984  cardinfima  10019  dfacacn  10064  cfflb  10181  cofsmo  10191  cfcoflem  10194  coftr  10195  fin23lem40  10273  axdc3lem2  10373  ac6num  10401  ac6c4  10403  ac6s2  10408  ttukeylem6  10436  iunfo  10461  pwcfsdom  10506  fpwwe2lem5  10558  fpwwe2lem7  10560  pwfseqlem3  10583  inar1  10698  tskcard  10704  tskuni  10706  tskurn  10712  gruima  10725  nqerrel  10855  recmulnq  10887  dmrecnq  10891  axpre-sup  11092  ofsubeq0  12154  dfz2  12519  uzn0  12780  rpnnen1lem3  12904  rpnnen1lem5  12906  unirnioo  13377  dfioo2  13378  ioorebas  13379  fseq1p1m1  13526  2ffzeq  13577  fvinim0ffz  13717  injresinjlem  13718  fsequb2  13911  fseqsupcl  13912  fseqsupubi  13913  ser0f  13990  hashgval  14268  hashinf  14270  hashresfn  14275  ffz0hash  14382  fnfzo0hash  14385  wrdred1hash  14496  revlen  14697  revrev  14702  repswlen  14711  repsdf2  14713  cshword  14726  0csh0  14728  lenco  14767  s1co  14768  cshco  14771  swrdco  14772  s7f1o  14901  ofccat  14904  shftf  15014  uzin2  15280  rexanuz  15281  limsuple  15413  limsupval2  15415  rlimres  15493  lo1res  15494  rlimresb  15500  isercolllem2  15601  isercolllem3  15602  isercoll  15603  supcvg  15791  prodf1f  15827  eff2  16036  reeff1  16057  tanval  16065  ruclem4  16171  ruclem12  16178  prmreclem6  16861  1arithlem4  16866  1arith  16867  vdwmc  16918  vdwlem1  16921  vdwlem8  16928  vdwlem13  16933  ramval  16948  0ram  16960  0ram2  16961  0ramcl  16963  ramcl  16969  fsets  17108  firest  17364  0ssc  17773  0subcat  17774  isfull2  17849  arwhoma  17981  gsumval2a  18622  isgrpinv  18935  kerf1ghm  19188  f1omvdconj  19387  pmtrmvd  19397  pmtrfinv  19402  pmtrdifellem4  19420  efgsfo  19680  efgredlem  19688  efgcpbllemb  19696  frgpup3lem  19718  0frgp  19720  gexex  19794  torsubg  19795  gsumval3  19848  gsumzres  19850  gsummptmhm  19881  gsumzoppg  19885  dprdf1o  19975  dprd2db  19986  zrinitorngc  20587  zrtermorngc  20588  zrtermoringc  20620  srngf1o  20793  lmhmima  21011  lmhmpreima  21012  lmhmrnlss  21014  lspextmo  21020  pwssplit1  21023  cnfldadd  21327  cnfldmul  21329  dfcnfldOLD  21337  cnfldplusf  21363  cnfldsub  21364  chrrhm  21498  znunit  21530  psgnevpmb  21554  psgndiflemB  21567  mpofrlmd  21744  frlmipval  21746  frlmphl  21748  frlmlbs  21764  frlmup4  21768  ellspd  21769  lindfmm  21794  lsslindf  21797  psrbaglefi  21894  psrlidm  21929  mplmonmul  22003  evlseu  22050  mpfconst  22076  mpfproj  22077  mpfsubrg  22078  coe1sclmulfv  22237  pf1const  22302  pf1id  22303  pf1subrg  22304  mpfpf1  22307  pf1mpf  22308  mamuass  22358  mamudi  22359  mamudir  22360  mamuvs1  22361  mamuvs2  22362  1mavmul  22504  mavmulass  22505  mdetunilem7  22574  madutpos  22598  lecldbas  23175  lmbr2  23215  cncnpi  23234  cncnp  23236  cnpdis  23249  lmff  23257  pnrmopn  23299  dnsconst  23334  cmpsub  23356  tgcmp  23357  hauscmplem  23362  2ndcctbss  23411  2ndcomap  23414  2ndcsep  23415  1stccnp  23418  kgenidm  23503  iskgen2  23504  1stckgen  23510  kgen2cn  23515  ptpjpre1  23527  pttop  23538  ptuni  23550  ptval2  23557  tx1cn  23565  tx2cn  23566  ptpjcn  23567  ptpjopn  23568  ptclsg  23571  ptcnplem  23577  upxp  23579  txcnmpt  23580  uptx  23581  txcmplem2  23598  txkgen  23608  xkoptsub  23610  xkopt  23611  xkococnlem  23615  xkococn  23616  ptcmpfi  23769  zfbas  23852  uzrest  23853  rnelfmlem  23908  rnelfm  23909  fmfnfmlem2  23911  fmfnfm  23914  lmflf  23961  alexsubALT  24007  clssubg  24065  qustgplem  24077  tsmsres  24100  tsmsxplem1  24109  ucncn  24240  xmettpos  24305  imasdsf1olem  24329  blrnps  24364  blrn  24365  xmeterval  24388  tmslem  24438  tmsxms  24442  imasf1oxms  24445  prdsxms  24486  blval2  24518  metuel2  24521  isngp2  24553  isngp3  24554  tngngp2  24608  isnghm  24679  qtopbaslem  24714  qdensere  24725  cnbl0  24729  cnblcld  24730  cnfldms  24731  blssioo  24751  tgioo  24752  tgqioo  24756  xrtgioo  24763  xrsdsre  24767  xrge0tsms  24791  iimulcnOLD  24903  bndth  24925  lebnumlem3  24930  nmhmcn  25088  cphsqrtcl  25152  lmmbr2  25227  caucfil  25251  causs  25266  lmcau  25281  bcth3  25299  cncms  25323  cnfldcusp  25325  rrxmvallem  25372  ivthicc  25427  ovolfioo  25436  ovolficc  25437  ovolficcss  25438  ovollb2lem  25457  ovoliunlem2  25472  ovolshftlem1  25478  ovolicc2  25491  ismbl  25495  voliunlem2  25520  volsup  25525  ioorf  25542  ioorinv  25545  ioorcl  25546  uniiccdif  25547  uniioovol  25548  uniiccvol  25549  uniioombllem2  25552  uniioombllem4  25555  dyaddisj  25565  dyadmax  25567  dyadmbllem  25568  dyadmbl  25569  opnmbllem  25570  opnmblALT  25572  volsup2  25574  mbfdm  25595  mbfima  25599  mbfid  25604  ismbfd  25608  mbfres2  25614  mbfposr  25621  mbfimaopnlem  25624  mbflimsup  25635  0plef  25641  i1f1lem  25658  itg11  25660  itg1addlem4  25668  i1fpos  25675  itg1le  25682  itg1climres  25683  mbfi1fseqlem5  25688  mbfi1flimlem  25691  xrge0f  25700  itg2ge0  25704  itg2seq  25711  itg2i1fseqle  25723  itg2i1fseq2  25725  itg2addlem  25727  itg2gt0  25729  limciun  25863  dvres  25880  dvres3a  25883  cpnres  25907  dvfre  25923  dvmptres3  25928  dvlip2  25968  dvgt0lem2  25976  deg1fvi  26058  uc1pmon1p  26125  fta1g  26143  ig1peu  26148  ig1pdvds  26153  plyco0  26165  plypf1  26185  dgrlem  26202  dgrub  26207  dgrlb  26209  coemulc  26228  plyreres  26258  plydivlem3  26271  plydivlem4  26272  plydiveu  26274  plyremlem  26280  fta1lem  26283  fta1  26284  vieta1lem2  26287  plyexmo  26289  elaa  26292  elqaalem3  26297  aannenlem1  26304  pserulm  26399  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  26725  cxpcn3  26726  resqrtcn  26727  asinneg  26864  areambl  26936  emcllem7  26980  lgamgulm2  27014  basellem4  27062  sqff1o  27160  mpodvdsmulf1o  27172  fsumdvdsmul  27173  dvdsmulf1o  27174  fsumdvdsmulOLD  27175  ostthlem1  27606  ostth  27618  noetasuplem4  27716  madeval2  27841  elold  27867  old1  27873  madeoldsuc  27893  tglnfn  28631  f1otrg  28955  axlowdimlem6  29032  axlowdimlem8  29034  axlowdimlem9  29035  axlowdimlem11  29037  axlowdimlem12  29038  axlowdimlem17  29043  elntg2  29070  dfpth2  29814  cyclnumvtx  29885  crctcshlem4  29905  clwlkclwwlklem2  30087  eucrct2eupth  30332  ex-fpar  30549  cnnvm  30770  sspmlem  30820  nvo00  30849  nmlno0lem  30881  phoeqi  30945  ubthlem1  30958  hhip  31265  hhssabloilem  31349  hhssnv  31352  hhsssh  31357  occllem  31391  shsel  31402  chscllem2  31726  df0op2  31840  hoeq  31848  hocofni  31855  hoaddfni  31858  hosubfni  31859  hon0  31881  ho01i  31916  hoeq1  31918  elnlfn  32016  nmlnop0iALT  32083  lnopco0i  32092  imaelshi  32146  nlelchi  32149  rnbra  32195  cnvbraval  32198  kbass5  32208  hmopidmchi  32239  hmopidmpji  32240  foresf1o  32591  fcomptf  32748  ofpreima  32755  resf1o  32820  maprnin  32821  fpwrelmapffslem  32822  hashgt1  32899  indpi1  32952  indpreima  32958  s3clhash  33041  gsumpart  33157  xrge0tsmsd  33167  tocyc01  33212  cyc3evpm  33244  cycpmgcl  33247  cycpmconjslem2  33249  cyc3conja  33251  kerunit  33418  1arithidomlem1  33628  1arithidomlem2  33629  1arithidom  33630  psrmonmul  33727  dimval  33778  dimvalfi  33779  ply1degltdimlem  33800  ply1degltdim  33801  elirng  33864  txomap  34012  locfinreflem  34018  hauseqcn  34076  xpinpreima  34084  xpinpreima2  34085  tpr2rico  34090  mndpluscn  34104  raddcn  34107  xrge0pluscn  34118  xrge0tmdALT  34124  rge0scvg  34127  pl1cn  34133  elzrhunit  34155  qqhf  34164  cnrrext  34188  qqhre  34198  1stmbfm  34438  2ndmbfm  34439  mbfmcnt  34446  omssubadd  34478  carsggect  34496  eulerpartlemsv2  34536  eulerpartlems  34538  eulerpartlemv  34542  eulerpartlemb  34546  eulerpartlemf  34548  eulerpartlemt  34549  eulerpartlemmf  34553  eulerpartlemgvv  34554  eulerpartlemgh  34556  eulerpartlemgs2  34558  sseqmw  34569  sseqf  34570  sseqp1  34573  fiblem  34576  fibp1  34579  plymul02  34724  signsvtn0  34748  signstres  34753  signshlen  34768  reprinrn  34796  circlemethhgt  34821  txsconnlem  35456  iccllysconn  35466  rellysconn  35467  cvmseu  35492  cvmliftmolem2  35498  cvmliftlem6  35506  cvmliftlem7  35507  cvmliftlem8  35508  cvmliftlem9  35509  cvmliftlem11  35511  cvmliftlem15  35514  cvmlift2lem7  35525  cvmlift2lem10  35528  cvmlift3lem8  35542  cvmlift3lem9  35543  mvrsfpw  35722  mrsubff1  35730  msrid  35761  msrfo  35762  elmsta  35764  mtyf  35768  msubff1  35772  vhmcls  35782  mclsax  35785  elmthm  35792  mthmblem  35796  mclsppslem  35799  iprodefisumlem  35956  fullfunfnv  36162  fullfunfv  36163  tailfb  36593  filnetlem4  36597  regsfromunir1  36692  taupilem3  37574  icoreresf  37607  icoreelrnab  37609  relowlssretop  37618  relowlpssretop  37619  unccur  37854  matunitlindflem1  37867  matunitlindflem2  37868  ptrecube  37871  poimirlem28  37899  poimirlem32  37903  heicant  37906  opnmbllem0  37907  mblfinlem1  37908  mblfinlem2  37909  volsupnfl  37916  cnambfre  37919  dvtan  37921  itg2addnclem  37922  itg2addnclem2  37923  ftc1anclem3  37946  ftc1anclem5  37948  ftc1anclem7  37950  ftc1anclem8  37951  ftc1anc  37952  areacirc  37964  indexdom  37985  sdclem2  37993  sstotbnd2  38025  sstotbnd  38026  isbndx  38033  isbnd3b  38036  prdsbnd  38044  prdstotbnd  38045  ismtyhmeolem  38055  heibor1lem  38060  heiborlem1  38062  heibor  38072  rrnequiv  38086  keridl  38283  ellkr  39465  lkr0f  39470  cdleme50rnlem  40920  aks6d1c2lem4  42497  aks6d1c5  42509  sticksstones11  42526  sticksstones19  42535  sticksstones22  42538  aks6d1c6lem4  42543  aks6d1c6isolem2  42545  fsuppind  42948  elrfirn  43052  ismrcd2  43056  isnacs2  43063  nacsfix  43069  mapfzcons1  43074  mzpcompact2lem  43108  eq0rabdioph  43133  eldioph4b  43168  diophren  43170  pw2f1ocnv  43394  pw2f1o2val2  43397  lmhmfgsplit  43443  pwssplit4  43446  hbt  43487  mpaaeu  43507  mendring  43545  proot1mul  43551  proot1hash  43552  proot1ex  43553  deg1mhm  43557  fgraphopab  43560  hausgraph  43562  nvocnvb  43778  ofsubid  44680  expgrowthi  44689  expgrowth  44691  binomcxplemdvbinom  44709  binomcxplemcvg  44710  binomcxplemnotnn0  44712  relpfrlem  45309  rfcnpre1  45379  rfcnpre2  45391  cncmpmax  45392  rfcnpre3  45393  rfcnpre4  45394  elixpconstg  45448  ffi  45532  islptre  45979  resincncf  46233  dvcosre  46270  dvresntr  46276  volioof  46345  stoweidlem48  46406  fourierdlem12  46477  fourierdlem15  46480  fourierdlem41  46506  fourierdlem42  46507  fourierdlem46  46510  fourierdlem48  46512  fourierdlem49  46513  fourierdlem54  46518  fourierdlem56  46520  fourierdlem62  46526  fourierdlem64  46528  fourierdlem65  46529  fourierdlem73  46537  fourierdlem74  46538  fourierdlem75  46539  fourierdlem102  46566  fourierdlem103  46567  fourierdlem104  46568  fourierdlem114  46578  sge0split  46767  elhoi  46900  mbfresmf  47097  cjnpoly  47249  cfsetsnfsetf1  47419  cfsetsnfsetfo  47420  focofob  47440  f1ocof1ob  47441  fafvelcdm  47530  ffnafv  47531  fafv2elcdm  47594  fafv2elrnb  47595  imarnf1pr  47642  2ffzoeq  47687  fundcmpsurbijinjpreimafv  47767  fundcmpsurinjimaid  47771  fargshiftfv  47799  fargshiftf  47800  fargshiftf1  47801  fargshiftfo  47802  cycl3grtri  48307  fdmdifeqresdif  48702  fdivmpt  48900  fdivmptf  48901  refdivmptf  48902  1arymaptf1  49002  2arymaptf1  49013  ackfnnn0  49045  homf0  49368  aacllem  50160