Theorem ffn 6609

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

Syntax hints:   → wi 4   ⊆ wss 3888  ran crn 5591   Fn wfn 6432  ⟶wf 6433

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 206  df-an 397  df-f 6441

This theorem is referenced by:  ffnd  6610  ffun  6612  frel  6614  fdm  6618  fdmOLD  6619  ffrn  6623  fresin  6652  fresaun  6654  fresaunres2  6655  fcoi1  6657  feu  6659  f0bi  6666  dffo2  6701  fimadmfo  6706  feqmptdf  6848  fvco3  6876  ffvelrn  6968  dff2  6984  dffo3  6987  dffo4  6988  dffo5  6989  f1ompt  6994  ffnfv  7001  frnssb  7004  fcompt  7014  fsn2  7017  fprb  7078  fconst2g  7087  fpr2g  7096  fex  7111  dff13  7137  nvocnv  7162  soisores  7207  fdmexb  7765  fo1stres  7866  fo2ndres  7867  1stcof  7870  2ndcof  7871  curry1f  7955  curry2f  7957  fparlem1  7961  fparlem2  7962  fo2ndf  7971  tposf2  8075  smo11  8204  fsetexb  8661  mapsnd  8683  pw2f1olem  8872  mapen  8937  mapunen  8942  fissuni  9133  fipreima  9134  indexfi  9136  mapfien  9176  oismo  9308  cantnflt  9439  cantnfp1lem3  9447  cantnflem4  9459  tcrank  9651  updjudhcoinlf  9699  updjudhcoinrg  9700  updjud  9701  infpwfien  9827  cardinfima  9862  dfacacn  9906  cfflb  10024  cofsmo  10034  cfcoflem  10037  coftr  10038  fin23lem40  10116  axdc3lem2  10216  ac6num  10244  ac6c4  10246  ac6s2  10251  ttukeylem6  10279  iunfo  10304  pwcfsdom  10348  fpwwe2lem5  10400  fpwwe2lem7  10402  pwfseqlem3  10425  inar1  10540  tskcard  10546  tskuni  10548  tskurn  10554  gruima  10567  nqerrel  10697  recmulnq  10729  dmrecnq  10733  axpre-sup  10934  ofsubeq0  11979  dfz2  12347  uzn0  12608  rpnnen1lem3  12728  rpnnen1lem5  12730  unirnioo  13190  dfioo2  13191  ioorebas  13192  fseq1p1m1  13339  2ffzeq  13386  fvinim0ffz  13515  injresinjlem  13516  fsequb2  13705  fseqsupcl  13706  fseqsupubi  13707  ser0f  13785  hashgval  14056  hashinf  14058  hashresfn  14063  ffz0hash  14168  fnfzo0hash  14171  wrdred1hash  14273  revlen  14484  revrev  14489  repswlen  14498  repsdf2  14500  cshword  14513  0csh0  14515  lenco  14554  s1co  14555  cshco  14558  swrdco  14559  ofccat  14689  shftf  14799  uzin2  15065  rexanuz  15066  limsuple  15196  limsupval2  15198  rlimres  15276  lo1res  15277  rlimresb  15283  isercolllem2  15386  isercolllem3  15387  isercoll  15388  supcvg  15577  prodf1f  15613  eff2  15817  reeff1  15838  tanval  15846  ruclem4  15952  ruclem12  15959  prmreclem6  16631  1arithlem4  16636  1arith  16637  vdwmc  16688  vdwlem1  16691  vdwlem8  16698  vdwlem13  16703  ramval  16718  0ram  16730  0ram2  16731  0ramcl  16733  ramcl  16739  fsets  16879  firest  17152  0ssc  17561  0subcat  17562  isfull2  17636  arwhoma  17769  gsumval2a  18378  isgrpinv  18641  f1omvdconj  19063  pmtrmvd  19073  pmtrfinv  19078  pmtrdifellem4  19096  efgsfo  19354  efgredlem  19362  efgcpbllemb  19370  frgpup3lem  19392  0frgp  19394  gexex  19463  torsubg  19464  gsumval3  19517  gsumzres  19519  gsummptmhm  19550  gsumzoppg  19554  dprdf1o  19644  dprd2db  19655  kerf1ghm  19996  srngf1o  20123  lmhmima  20318  lmhmpreima  20319  lmhmrnlss  20321  lspextmo  20327  pwssplit1  20330  cnfldplusf  20634  cnfldsub  20635  chrrhm  20744  znunit  20780  psgnevpmb  20801  psgndiflemB  20814  mpofrlmd  20993  frlmipval  20995  frlmphl  20997  frlmlbs  21013  frlmup4  21017  ellspd  21018  lindfmm  21043  lsslindf  21046  psrbaglefi  21144  psrbaglefiOLD  21145  psrlidm  21181  mplmonmul  21246  evlseu  21302  mpfconst  21320  mpfproj  21321  mpfsubrg  21322  coe1sclmulfv  21463  pf1const  21521  pf1id  21522  pf1subrg  21523  mpfpf1  21526  pf1mpf  21527  mamuass  21558  mamudi  21559  mamudir  21560  mamuvs1  21561  mamuvs2  21562  1mavmul  21706  mavmulass  21707  mdetunilem7  21776  madutpos  21800  lecldbas  22379  lmbr2  22419  cncnpi  22438  cncnp  22440  cnpdis  22453  lmff  22461  pnrmopn  22503  dnsconst  22538  cmpsub  22560  tgcmp  22561  hauscmplem  22566  2ndcctbss  22615  2ndcomap  22618  2ndcsep  22619  1stccnp  22622  kgenidm  22707  iskgen2  22708  1stckgen  22714  kgen2cn  22719  ptpjpre1  22731  pttop  22742  ptuni  22754  ptval2  22761  tx1cn  22769  tx2cn  22770  ptpjcn  22771  ptpjopn  22772  ptclsg  22775  ptcnplem  22781  upxp  22783  txcnmpt  22784  uptx  22785  txcmplem2  22802  txkgen  22812  xkoptsub  22814  xkopt  22815  xkococnlem  22819  xkococn  22820  ptcmpfi  22973  zfbas  23056  uzrest  23057  rnelfmlem  23112  rnelfm  23113  fmfnfmlem2  23115  fmfnfm  23118  lmflf  23165  alexsubALT  23211  clssubg  23269  qustgplem  23281  tsmsres  23304  tsmsxplem1  23313  ucncn  23446  xmettpos  23511  imasdsf1olem  23535  blrnps  23570  blrn  23571  xmeterval  23594  tmslem  23646  tmslemOLD  23647  tmsxms  23651  imasf1oxms  23654  prdsxms  23695  blval2  23727  metuel2  23730  isngp2  23762  isngp3  23763  tngngp2  23825  isnghm  23896  qtopbaslem  23931  qdensere  23942  cnbl0  23946  cnblcld  23947  cnfldms  23948  blssioo  23967  tgioo  23968  tgqioo  23972  xrtgioo  23978  xrsdsre  23982  xrge0tsms  24006  iimulcn  24110  bndth  24130  lebnumlem3  24135  nmhmcn  24292  cphsqrtcl  24357  lmmbr2  24432  caucfil  24456  causs  24471  lmcau  24486  bcth3  24504  cncms  24528  cnfldcusp  24530  rrxmvallem  24577  ivthicc  24631  ovolfioo  24640  ovolficc  24641  ovolficcss  24642  ovollb2lem  24661  ovoliunlem2  24676  ovolshftlem1  24682  ovolicc2  24695  ismbl  24699  voliunlem2  24724  volsup  24729  ioorf  24746  ioorinv  24749  ioorcl  24750  uniiccdif  24751  uniioovol  24752  uniiccvol  24753  uniioombllem2  24756  uniioombllem4  24759  dyaddisj  24769  dyadmax  24771  dyadmbllem  24772  dyadmbl  24773  opnmbllem  24774  opnmblALT  24776  volsup2  24778  mbfdm  24799  mbfima  24803  mbfid  24808  ismbfd  24812  mbfres2  24818  mbfposr  24825  mbfimaopnlem  24828  mbflimsup  24839  0plef  24845  i1f1lem  24862  itg11  24864  itg1addlem4  24872  itg1addlem4OLD  24873  i1fpos  24880  itg1le  24887  itg1climres  24888  mbfi1fseqlem5  24893  mbfi1flimlem  24896  xrge0f  24905  itg2ge0  24909  itg2seq  24916  itg2i1fseqle  24928  itg2i1fseq2  24930  itg2addlem  24932  itg2gt0  24934  limciun  25067  dvres  25084  dvres3a  25087  cpnres  25110  dvfre  25124  dvmptres3  25129  dvlip2  25168  dvgt0lem2  25176  deg1fvi  25259  uc1pmon1p  25325  fta1g  25341  ig1peu  25345  ig1pdvds  25350  plyco0  25362  plypf1  25382  dgrlem  25399  dgrub  25404  dgrlb  25406  coemulc  25425  plyreres  25452  plydivlem3  25464  plydivlem4  25465  plydiveu  25467  plyremlem  25473  fta1lem  25476  fta1  25477  vieta1lem2  25480  plyexmo  25482  elaa  25485  elqaalem3  25490  aannenlem1  25497  pserulm  25590  psercnlem2  25592  psercnlem1  25593  psercn  25594  abelth  25609  reeff1o  25615  pilem1  25619  recosf1o  25700  resinf1o  25701  efif1olem3  25709  efif1olem4  25710  efifo  25712  eff1olem  25713  ellogrn  25724  logcn  25811  dvloglem  25812  logf1o2  25814  efopnlem1  25820  efopnlem2  25821  efopn  25822  logtayl  25824  cxpcn3lem  25909  cxpcn3  25910  resqrtcn  25911  asinneg  26045  areambl  26117  emcllem7  26160  lgamgulm2  26194  basellem4  26242  sqff1o  26340  dvdsmulf1o  26352  fsumdvdsmul  26353  ostthlem1  26784  ostth  26796  tglnfn  26917  f1otrg  27241  axlowdimlem6  27324  axlowdimlem8  27326  axlowdimlem9  27327  axlowdimlem11  27329  axlowdimlem12  27330  axlowdimlem17  27335  elntg2  27362  crctcshlem4  28194  clwlkclwwlklem2  28373  eucrct2eupth  28618  ex-fpar  28835  cnnvm  29053  sspmlem  29103  nvo00  29132  nmlno0lem  29164  phoeqi  29228  ubthlem1  29241  hhip  29548  hhssabloilem  29632  hhssnv  29635  hhsssh  29640  occllem  29674  shsel  29685  chscllem2  30009  df0op2  30123  hoeq  30131  hocofni  30138  hoaddfni  30141  hosubfni  30142  hon0  30164  ho01i  30199  hoeq1  30201  elnlfn  30299  nmlnop0iALT  30366  lnopco0i  30375  imaelshi  30429  nlelchi  30432  rnbra  30478  cnvbraval  30481  kbass5  30491  hmopidmchi  30522  hmopidmpji  30523  foresf1o  30859  fimarab  30989  fcomptf  31004  ofpreima  31011  resf1o  31074  maprnin  31075  fpwrelmapffslem  31076  hashgt1  31137  s3clhash  31231  gsumpart  31324  xrge0tsmsd  31326  tocyc01  31394  cyc3evpm  31426  cycpmgcl  31429  cycpmconjslem2  31431  cyc3conja  31433  kerunit  31531  dimval  31695  dimvalfi  31696  txomap  31793  locfinreflem  31799  hauseqcn  31857  xpinpreima  31865  xpinpreima2  31866  tpr2rico  31871  mndpluscn  31885  rmulccn  31887  raddcn  31888  xrge0pluscn  31899  xrge0tmdALT  31905  rge0scvg  31908  pl1cn  31914  elzrhunit  31938  qqhf  31945  cnrrext  31969  qqhre  31979  indpi1  31997  indpreima  32002  1stmbfm  32236  2ndmbfm  32237  mbfmcnt  32244  omssubadd  32276  carsggect  32294  eulerpartlemsv2  32334  eulerpartlems  32336  eulerpartlemv  32340  eulerpartlemb  32344  eulerpartlemf  32346  eulerpartlemt  32347  eulerpartlemmf  32351  eulerpartlemgvv  32352  eulerpartlemgh  32354  eulerpartlemgs2  32356  sseqmw  32367  sseqf  32368  sseqp1  32371  fiblem  32374  fibp1  32377  plymul02  32534  signsvtn0  32558  signstres  32563  signshlen  32578  reprinrn  32607  circlemethhgt  32632  txsconnlem  33211  iccllysconn  33221  rellysconn  33222  cvmseu  33247  cvmliftmolem2  33253  cvmliftlem6  33261  cvmliftlem7  33262  cvmliftlem8  33263  cvmliftlem9  33264  cvmliftlem11  33266  cvmliftlem15  33269  cvmlift2lem7  33280  cvmlift2lem10  33283  cvmlift3lem8  33297  cvmlift3lem9  33298  mvrsfpw  33477  mrsubff1  33485  msrid  33516  msrfo  33517  elmsta  33519  mtyf  33523  msubff1  33527  vhmcls  33537  mclsax  33540  elmthm  33547  mthmblem  33551  mclsppslem  33554  iprodefisumlem  33715  soseq  33812  noetasuplem4  33948  madeval2  34046  elold  34062  madeoldsuc  34076  fullfunfnv  34257  fullfunfv  34258  tailfb  34575  filnetlem4  34579  taupilem3  35499  icoreresf  35532  icoreelrnab  35534  relowlssretop  35543  relowlpssretop  35544  unccur  35769  matunitlindflem1  35782  matunitlindflem2  35783  ptrecube  35786  poimirlem28  35814  poimirlem32  35818  heicant  35821  opnmbllem0  35822  mblfinlem1  35823  mblfinlem2  35824  volsupnfl  35831  cnambfre  35834  dvtan  35836  itg2addnclem  35837  itg2addnclem2  35838  ftc1anclem3  35861  ftc1anclem5  35863  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  areacirc  35879  indexdom  35901  sdclem2  35909  sstotbnd2  35941  sstotbnd  35942  isbndx  35949  isbnd3b  35952  prdsbnd  35960  prdstotbnd  35961  ismtyhmeolem  35971  heibor1lem  35976  heiborlem1  35978  heibor  35988  rrnequiv  36002  keridl  36199  ellkr  37110  lkr0f  37115  cdleme50rnlem  38565  sticksstones11  40119  sticksstones19  40128  sticksstones22  40131  fsuppind  40286  elrfirn  40524  ismrcd2  40528  isnacs2  40535  nacsfix  40541  mapfzcons1  40546  mzpcompact2lem  40580  eq0rabdioph  40605  eldioph4b  40640  diophren  40642  pw2f1ocnv  40866  pw2f1o2val2  40869  lmhmfgsplit  40918  pwssplit4  40921  hbt  40962  mpaaeu  40982  mendring  41024  proot1mul  41031  proot1hash  41032  proot1ex  41033  deg1mhm  41039  fgraphopab  41042  hausgraph  41044  ofsubid  41949  expgrowthi  41958  expgrowth  41960  binomcxplemdvbinom  41978  binomcxplemcvg  41979  binomcxplemnotnn0  41981  rfcnpre1  42569  rfcnpre2  42581  cncmpmax  42582  rfcnpre3  42583  rfcnpre4  42584  elixpconstg  42646  ffi  42716  dffo3f  42724  islptre  43167  resincncf  43423  dvcosre  43460  dvresntr  43466  volioof  43535  stoweidlem48  43596  fourierdlem12  43667  fourierdlem15  43670  fourierdlem41  43696  fourierdlem42  43697  fourierdlem46  43700  fourierdlem48  43702  fourierdlem49  43703  fourierdlem54  43708  fourierdlem56  43710  fourierdlem62  43716  fourierdlem64  43718  fourierdlem65  43719  fourierdlem73  43727  fourierdlem74  43728  fourierdlem75  43729  fourierdlem102  43756  fourierdlem103  43757  fourierdlem104  43758  fourierdlem114  43768  sge0split  43954  elhoi  44087  mbfresmf  44284  cfsetsnfsetf1  44564  cfsetsnfsetfo  44565  focofob  44583  f1ocof1ob  44584  fafvelrn  44673  ffnafv  44674  fafv2elrn  44737  fafv2elrnb  44738  imarnf1pr  44785  2ffzoeq  44831  fundcmpsurbijinjpreimafv  44870  fundcmpsurinjimaid  44874  fargshiftfv  44902  fargshiftf  44903  fargshiftf1  44904  fargshiftfo  44905  zrinitorngc  45569  zrtermorngc  45570  zrtermoringc  45639  fdmdifeqresdif  45688  fdivmpt  45897  fdivmptf  45898  refdivmptf  45899  1arymaptf1  45999  2arymaptf1  46010  ackfnnn0  46042  aacllem  46516