Theorem ffn 6584

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

Syntax hints:   → wi 4   ⊆ wss 3883  ran crn 5581   Fn wfn 6413  ⟶wf 6414

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 396  df-f 6422

This theorem is referenced by:  ffnd  6585  ffun  6587  frel  6589  fdm  6593  fdmOLD  6594  ffrn  6598  fresin  6627  fresaun  6629  fresaunres2  6630  fcoi1  6632  feu  6634  f0bi  6641  dffo2  6676  fimadmfo  6681  feqmptdf  6821  fvco3  6849  ffvelrn  6941  dff2  6957  dffo3  6960  dffo4  6961  dffo5  6962  f1ompt  6967  ffnfv  6974  frnssb  6977  fcompt  6987  fsn2  6990  fprb  7051  fconst2g  7060  fpr2g  7069  fex  7084  dff13  7109  nvocnv  7134  soisores  7178  fdmexb  7730  fo1stres  7830  fo2ndres  7831  1stcof  7834  2ndcof  7835  curry1f  7917  curry2f  7919  fparlem1  7923  fparlem2  7924  fo2ndf  7933  tposf2  8037  smo11  8166  fsetexb  8610  mapsnd  8632  pw2f1olem  8816  mapen  8877  mapunen  8882  fissuni  9054  fipreima  9055  indexfi  9057  mapfien  9097  oismo  9229  cantnflt  9360  cantnfp1lem3  9368  cantnflem4  9380  tcrank  9573  updjudhcoinlf  9621  updjudhcoinrg  9622  updjud  9623  infpwfien  9749  cardinfima  9784  dfacacn  9828  cfflb  9946  cofsmo  9956  cfcoflem  9959  coftr  9960  fin23lem40  10038  axdc3lem2  10138  ac6num  10166  ac6c4  10168  ac6s2  10173  ttukeylem6  10201  iunfo  10226  pwcfsdom  10270  fpwwe2lem5  10322  fpwwe2lem7  10324  pwfseqlem3  10347  inar1  10462  tskcard  10468  tskuni  10470  tskurn  10476  gruima  10489  nqerrel  10619  recmulnq  10651  dmrecnq  10655  axpre-sup  10856  ofsubeq0  11900  dfz2  12268  uzn0  12528  rpnnen1lem3  12648  rpnnen1lem5  12650  unirnioo  13110  dfioo2  13111  ioorebas  13112  fseq1p1m1  13259  2ffzeq  13306  fvinim0ffz  13434  injresinjlem  13435  fsequb2  13624  fseqsupcl  13625  fseqsupubi  13626  ser0f  13704  hashgval  13975  hashinf  13977  hashresfn  13982  ffz0hash  14087  fnfzo0hash  14090  wrdred1hash  14192  revlen  14403  revrev  14408  repswlen  14417  repsdf2  14419  cshword  14432  0csh0  14434  lenco  14473  s1co  14474  cshco  14477  swrdco  14478  ofccat  14608  shftf  14718  uzin2  14984  rexanuz  14985  limsuple  15115  limsupval2  15117  rlimres  15195  lo1res  15196  rlimresb  15202  isercolllem2  15305  isercolllem3  15306  isercoll  15307  supcvg  15496  prodf1f  15532  eff2  15736  reeff1  15757  tanval  15765  ruclem4  15871  ruclem12  15878  prmreclem6  16550  1arithlem4  16555  1arith  16556  vdwmc  16607  vdwlem1  16610  vdwlem8  16617  vdwlem13  16622  ramval  16637  0ram  16649  0ram2  16650  0ramcl  16652  ramcl  16658  fsets  16798  firest  17060  0ssc  17468  0subcat  17469  isfull2  17543  arwhoma  17676  gsumval2a  18284  isgrpinv  18547  f1omvdconj  18969  pmtrmvd  18979  pmtrfinv  18984  pmtrdifellem4  19002  efgsfo  19260  efgredlem  19268  efgcpbllemb  19276  frgpup3lem  19298  0frgp  19300  gexex  19369  torsubg  19370  gsumval3  19423  gsumzres  19425  gsummptmhm  19456  gsumzoppg  19460  dprdf1o  19550  dprd2db  19561  kerf1ghm  19902  srngf1o  20029  lmhmima  20224  lmhmpreima  20225  lmhmrnlss  20227  lspextmo  20233  pwssplit1  20236  cnfldplusf  20537  cnfldsub  20538  chrrhm  20647  znunit  20683  psgnevpmb  20704  psgndiflemB  20717  mpofrlmd  20894  frlmipval  20896  frlmphl  20898  frlmlbs  20914  frlmup4  20918  ellspd  20919  lindfmm  20944  lsslindf  20947  psrbaglefi  21045  psrbaglefiOLD  21046  psrlidm  21082  mplmonmul  21147  evlseu  21203  mpfconst  21221  mpfproj  21222  mpfsubrg  21223  coe1sclmulfv  21364  pf1const  21422  pf1id  21423  pf1subrg  21424  mpfpf1  21427  pf1mpf  21428  mamuass  21459  mamudi  21460  mamudir  21461  mamuvs1  21462  mamuvs2  21463  1mavmul  21605  mavmulass  21606  mdetunilem7  21675  madutpos  21699  lecldbas  22278  lmbr2  22318  cncnpi  22337  cncnp  22339  cnpdis  22352  lmff  22360  pnrmopn  22402  dnsconst  22437  cmpsub  22459  tgcmp  22460  hauscmplem  22465  2ndcctbss  22514  2ndcomap  22517  2ndcsep  22518  1stccnp  22521  kgenidm  22606  iskgen2  22607  1stckgen  22613  kgen2cn  22618  ptpjpre1  22630  pttop  22641  ptuni  22653  ptval2  22660  tx1cn  22668  tx2cn  22669  ptpjcn  22670  ptpjopn  22671  ptclsg  22674  ptcnplem  22680  upxp  22682  txcnmpt  22683  uptx  22684  txcmplem2  22701  txkgen  22711  xkoptsub  22713  xkopt  22714  xkococnlem  22718  xkococn  22719  ptcmpfi  22872  zfbas  22955  uzrest  22956  rnelfmlem  23011  rnelfm  23012  fmfnfmlem2  23014  fmfnfm  23017  lmflf  23064  alexsubALT  23110  clssubg  23168  qustgplem  23180  tsmsres  23203  tsmsxplem1  23212  ucncn  23345  xmettpos  23410  imasdsf1olem  23434  blrnps  23469  blrn  23470  xmeterval  23493  tmslem  23543  tmslemOLD  23544  tmsxms  23548  imasf1oxms  23551  prdsxms  23592  blval2  23624  metuel2  23627  isngp2  23659  isngp3  23660  tngngp2  23722  isnghm  23793  qtopbaslem  23828  qdensere  23839  cnbl0  23843  cnblcld  23844  cnfldms  23845  blssioo  23864  tgioo  23865  tgqioo  23869  xrtgioo  23875  xrsdsre  23879  xrge0tsms  23903  iimulcn  24007  bndth  24027  lebnumlem3  24032  nmhmcn  24189  cphsqrtcl  24253  lmmbr2  24328  caucfil  24352  causs  24367  lmcau  24382  bcth3  24400  cncms  24424  cnfldcusp  24426  rrxmvallem  24473  ivthicc  24527  ovolfioo  24536  ovolficc  24537  ovolficcss  24538  ovollb2lem  24557  ovoliunlem2  24572  ovolshftlem1  24578  ovolicc2  24591  ismbl  24595  voliunlem2  24620  volsup  24625  ioorf  24642  ioorinv  24645  ioorcl  24646  uniiccdif  24647  uniioovol  24648  uniiccvol  24649  uniioombllem2  24652  uniioombllem4  24655  dyaddisj  24665  dyadmax  24667  dyadmbllem  24668  dyadmbl  24669  opnmbllem  24670  opnmblALT  24672  volsup2  24674  mbfdm  24695  mbfima  24699  mbfid  24704  ismbfd  24708  mbfres2  24714  mbfposr  24721  mbfimaopnlem  24724  mbflimsup  24735  0plef  24741  i1f1lem  24758  itg11  24760  itg1addlem4  24768  itg1addlem4OLD  24769  i1fpos  24776  itg1le  24783  itg1climres  24784  mbfi1fseqlem5  24789  mbfi1flimlem  24792  xrge0f  24801  itg2ge0  24805  itg2seq  24812  itg2i1fseqle  24824  itg2i1fseq2  24826  itg2addlem  24828  itg2gt0  24830  limciun  24963  dvres  24980  dvres3a  24983  cpnres  25006  dvfre  25020  dvmptres3  25025  dvlip2  25064  dvgt0lem2  25072  deg1fvi  25155  uc1pmon1p  25221  fta1g  25237  ig1peu  25241  ig1pdvds  25246  plyco0  25258  plypf1  25278  dgrlem  25295  dgrub  25300  dgrlb  25302  coemulc  25321  plyreres  25348  plydivlem3  25360  plydivlem4  25361  plydiveu  25363  plyremlem  25369  fta1lem  25372  fta1  25373  vieta1lem2  25376  plyexmo  25378  elaa  25381  elqaalem3  25386  aannenlem1  25393  pserulm  25486  psercnlem2  25488  psercnlem1  25489  psercn  25490  abelth  25505  reeff1o  25511  pilem1  25515  recosf1o  25596  resinf1o  25597  efif1olem3  25605  efif1olem4  25606  efifo  25608  eff1olem  25609  ellogrn  25620  logcn  25707  dvloglem  25708  logf1o2  25710  efopnlem1  25716  efopnlem2  25717  efopn  25718  logtayl  25720  cxpcn3lem  25805  cxpcn3  25806  resqrtcn  25807  asinneg  25941  areambl  26013  emcllem7  26056  lgamgulm2  26090  basellem4  26138  sqff1o  26236  dvdsmulf1o  26248  fsumdvdsmul  26249  ostthlem1  26680  ostth  26692  tglnfn  26812  f1otrg  27136  axlowdimlem6  27218  axlowdimlem8  27220  axlowdimlem9  27221  axlowdimlem11  27223  axlowdimlem12  27224  axlowdimlem17  27229  elntg2  27256  crctcshlem4  28086  clwlkclwwlklem2  28265  eucrct2eupth  28510  ex-fpar  28727  cnnvm  28945  sspmlem  28995  nvo00  29024  nmlno0lem  29056  phoeqi  29120  ubthlem1  29133  hhip  29440  hhssabloilem  29524  hhssnv  29527  hhsssh  29532  occllem  29566  shsel  29577  chscllem2  29901  df0op2  30015  hoeq  30023  hocofni  30030  hoaddfni  30033  hosubfni  30034  hon0  30056  ho01i  30091  hoeq1  30093  elnlfn  30191  nmlnop0iALT  30258  lnopco0i  30267  imaelshi  30321  nlelchi  30324  rnbra  30370  cnvbraval  30373  kbass5  30383  hmopidmchi  30414  hmopidmpji  30415  foresf1o  30751  fimarab  30881  fcomptf  30897  ofpreima  30904  resf1o  30967  maprnin  30968  fpwrelmapffslem  30969  hashgt1  31030  s3clhash  31124  gsumpart  31217  xrge0tsmsd  31219  tocyc01  31287  cyc3evpm  31319  cycpmgcl  31322  cycpmconjslem2  31324  cyc3conja  31326  kerunit  31424  dimval  31588  dimvalfi  31589  txomap  31686  locfinreflem  31692  hauseqcn  31750  xpinpreima  31758  xpinpreima2  31759  tpr2rico  31764  mndpluscn  31778  rmulccn  31780  raddcn  31781  xrge0pluscn  31792  xrge0tmdALT  31798  rge0scvg  31801  pl1cn  31807  elzrhunit  31829  qqhf  31836  cnrrext  31860  qqhre  31870  indpi1  31888  indpreima  31893  1stmbfm  32127  2ndmbfm  32128  mbfmcnt  32135  omssubadd  32167  carsggect  32185  eulerpartlemsv2  32225  eulerpartlems  32227  eulerpartlemv  32231  eulerpartlemb  32235  eulerpartlemf  32237  eulerpartlemt  32238  eulerpartlemmf  32242  eulerpartlemgvv  32243  eulerpartlemgh  32245  eulerpartlemgs2  32247  sseqmw  32258  sseqf  32259  sseqp1  32262  fiblem  32265  fibp1  32268  plymul02  32425  signsvtn0  32449  signstres  32454  signshlen  32469  reprinrn  32498  circlemethhgt  32523  txsconnlem  33102  iccllysconn  33112  rellysconn  33113  cvmseu  33138  cvmliftmolem2  33144  cvmliftlem6  33152  cvmliftlem7  33153  cvmliftlem8  33154  cvmliftlem9  33155  cvmliftlem11  33157  cvmliftlem15  33160  cvmlift2lem7  33171  cvmlift2lem10  33174  cvmlift3lem8  33188  cvmlift3lem9  33189  mvrsfpw  33368  mrsubff1  33376  msrid  33407  msrfo  33408  elmsta  33410  mtyf  33414  msubff1  33418  vhmcls  33428  mclsax  33431  elmthm  33438  mthmblem  33442  mclsppslem  33445  iprodefisumlem  33612  soseq  33730  noetasuplem4  33866  madeval2  33964  elold  33980  madeoldsuc  33994  fullfunfnv  34175  fullfunfv  34176  tailfb  34493  filnetlem4  34497  taupilem3  35417  icoreresf  35450  icoreelrnab  35452  relowlssretop  35461  relowlpssretop  35462  unccur  35687  matunitlindflem1  35700  matunitlindflem2  35701  ptrecube  35704  poimirlem28  35732  poimirlem32  35736  heicant  35739  opnmbllem0  35740  mblfinlem1  35741  mblfinlem2  35742  volsupnfl  35749  cnambfre  35752  dvtan  35754  itg2addnclem  35755  itg2addnclem2  35756  ftc1anclem3  35779  ftc1anclem5  35781  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  areacirc  35797  indexdom  35819  sdclem2  35827  sstotbnd2  35859  sstotbnd  35860  isbndx  35867  isbnd3b  35870  prdsbnd  35878  prdstotbnd  35879  ismtyhmeolem  35889  heibor1lem  35894  heiborlem1  35896  heibor  35906  rrnequiv  35920  keridl  36117  ellkr  37030  lkr0f  37035  cdleme50rnlem  38485  sticksstones11  40040  sticksstones19  40049  sticksstones22  40052  fsuppind  40202  elrfirn  40433  ismrcd2  40437  isnacs2  40444  nacsfix  40450  mapfzcons1  40455  mzpcompact2lem  40489  eq0rabdioph  40514  eldioph4b  40549  diophren  40551  pw2f1ocnv  40775  pw2f1o2val2  40778  lmhmfgsplit  40827  pwssplit4  40830  hbt  40871  mpaaeu  40891  mendring  40933  proot1mul  40940  proot1hash  40941  proot1ex  40942  deg1mhm  40948  fgraphopab  40951  hausgraph  40953  ofsubid  41831  expgrowthi  41840  expgrowth  41842  binomcxplemdvbinom  41860  binomcxplemcvg  41861  binomcxplemnotnn0  41863  rfcnpre1  42451  rfcnpre2  42463  cncmpmax  42464  rfcnpre3  42465  rfcnpre4  42466  elixpconstg  42528  ffi  42598  dffo3f  42606  islptre  43050  resincncf  43306  dvcosre  43343  dvresntr  43349  volioof  43418  stoweidlem48  43479  fourierdlem12  43550  fourierdlem15  43553  fourierdlem41  43579  fourierdlem42  43580  fourierdlem46  43583  fourierdlem48  43585  fourierdlem49  43586  fourierdlem54  43591  fourierdlem56  43593  fourierdlem62  43599  fourierdlem64  43601  fourierdlem65  43602  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem114  43651  sge0split  43837  elhoi  43970  mbfresmf  44162  cfsetsnfsetf1  44440  cfsetsnfsetfo  44441  focofob  44459  f1ocof1ob  44460  fafvelrn  44549  ffnafv  44550  fafv2elrn  44613  fafv2elrnb  44614  imarnf1pr  44661  2ffzoeq  44708  fundcmpsurbijinjpreimafv  44747  fundcmpsurinjimaid  44751  fargshiftfv  44779  fargshiftf  44780  fargshiftf1  44781  fargshiftfo  44782  zrinitorngc  45446  zrtermorngc  45447  zrtermoringc  45516  fdmdifeqresdif  45565  fdivmpt  45774  fdivmptf  45775  refdivmptf  45776  1arymaptf1  45876  2arymaptf1  45887  ackfnnn0  45919  aacllem  46391