Theorem ffn 6514

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

Syntax hints:   → wi 4   ⊆ wss 3936  ran crn 5556   Fn wfn 6350  ⟶wf 6351

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 209  df-an 399  df-f 6359

This theorem is referenced by:  ffnd  6515  ffun  6517  frel  6519  fdm  6522  ffrn  6526  fresin  6547  fresaun  6549  fresaunres2  6550  fcoi1  6552  feu  6554  f0bi  6562  dffo2  6594  fimadmfo  6599  feqmptdf  6735  fvco3  6760  ffvelrn  6849  dff2  6865  dffo3  6868  dffo4  6869  dffo5  6870  f1ompt  6875  ffnfv  6882  frnssb  6885  fcompt  6895  fsn2  6898  fprb  6956  fconst2g  6965  fpr2g  6974  fex  6989  dff13  7013  nvocnv  7038  soisores  7080  fo1stres  7715  fo2ndres  7716  1stcof  7719  2ndcof  7720  curry1f  7801  curry2f  7803  fparlem1  7807  fparlem2  7808  fo2ndf  7817  tposf2  7916  smo11  8001  mapsnd  8450  pw2f1olem  8621  mapen  8681  mapunen  8686  fissuni  8829  fipreima  8830  indexfi  8832  mapfien  8871  oismo  9004  cantnflt  9135  cantnfp1lem3  9143  cantnflem4  9155  tcrank  9313  updjudhcoinlf  9361  updjudhcoinrg  9362  updjud  9363  infpwfien  9488  cardinfima  9523  dfacacn  9567  cfflb  9681  cofsmo  9691  cfcoflem  9694  coftr  9695  fin23lem40  9773  axdc3lem2  9873  ac6num  9901  ac6c4  9903  ac6s2  9908  ttukeylem6  9936  iunfo  9961  pwcfsdom  10005  fpwwe2lem6  10057  fpwwe2lem8  10059  pwfseqlem3  10082  inar1  10197  tskcard  10203  tskuni  10205  tskurn  10211  gruima  10224  nqerrel  10354  recmulnq  10386  dmrecnq  10390  axpre-sup  10591  ofsubeq0  11635  dfz2  12001  uzn0  12261  rpnnen1lem3  12379  rpnnen1lem5  12381  unirnioo  12838  dfioo2  12839  ioorebas  12840  fseq1p1m1  12982  2ffzeq  13029  fvinim0ffz  13157  injresinjlem  13158  fsequb2  13345  fseqsupcl  13346  fseqsupubi  13347  ser0f  13424  hashgval  13694  hashinf  13696  hashresfn  13701  ffz0hash  13806  fnfzo0hash  13809  wrdred1hash  13913  revlen  14124  revrev  14129  repswlen  14138  repsdf2  14140  cshword  14153  0csh0  14155  lenco  14194  s1co  14195  cshco  14198  swrdco  14199  ofccat  14329  shftf  14438  uzin2  14704  rexanuz  14705  limsuple  14835  limsupval2  14837  rlimres  14915  lo1res  14916  rlimresb  14922  isercolllem2  15022  isercolllem3  15023  isercoll  15024  supcvg  15211  prodf1f  15248  eff2  15452  reeff1  15473  tanval  15481  ruclem4  15587  ruclem12  15594  prmreclem6  16257  1arithlem4  16262  1arith  16263  vdwmc  16314  vdwlem1  16317  vdwlem8  16324  vdwlem13  16329  ramval  16344  0ram  16356  0ram2  16357  0ramcl  16359  ramcl  16365  fsets  16516  firest  16706  0ssc  17107  0subcat  17108  isfull2  17181  arwhoma  17305  gsumval2a  17895  isgrpinv  18156  f1omvdconj  18574  pmtrmvd  18584  pmtrfinv  18589  pmtrdifellem4  18607  efgsfo  18865  efgredlem  18873  efgcpbllemb  18881  frgpup3lem  18903  0frgp  18905  gexex  18973  torsubg  18974  gsumval3  19027  gsumzres  19029  gsummptmhm  19060  gsumzoppg  19064  dprdf1o  19154  dprd2db  19165  kerf1ghm  19497  kerf1hrmOLD  19498  srngf1o  19625  lmhmima  19819  lmhmpreima  19820  lmhmrnlss  19822  lspextmo  19828  pwssplit1  19831  psrbaglefi  20152  psrlidm  20183  mplmonmul  20245  evlseu  20296  mpfconst  20314  mpfproj  20315  mpfsubrg  20316  coe1sclmulfv  20451  pf1const  20509  pf1id  20510  pf1subrg  20511  mpfpf1  20514  pf1mpf  20515  cnfldplusf  20572  cnfldsub  20573  chrrhm  20678  znunit  20710  psgnevpmb  20731  psgndiflemB  20744  mpofrlmd  20921  frlmipval  20923  frlmphl  20925  frlmlbs  20941  frlmup4  20945  ellspd  20946  lindfmm  20971  lsslindf  20974  mamuass  21011  mamudi  21012  mamudir  21013  mamuvs1  21014  mamuvs2  21015  1mavmul  21157  mavmulass  21158  mdetunilem7  21227  madutpos  21251  lecldbas  21827  lmbr2  21867  cncnpi  21886  cncnp  21888  cnpdis  21901  lmff  21909  pnrmopn  21951  dnsconst  21986  cmpsub  22008  tgcmp  22009  hauscmplem  22014  2ndcctbss  22063  2ndcomap  22066  2ndcsep  22067  1stccnp  22070  kgenidm  22155  iskgen2  22156  1stckgen  22162  kgen2cn  22167  ptpjpre1  22179  pttop  22190  ptuni  22202  ptval2  22209  tx1cn  22217  tx2cn  22218  ptpjcn  22219  ptpjopn  22220  ptclsg  22223  ptcnplem  22229  upxp  22231  txcnmpt  22232  uptx  22233  txcmplem2  22250  txkgen  22260  xkoptsub  22262  xkopt  22263  xkococnlem  22267  xkococn  22268  ptcmpfi  22421  zfbas  22504  uzrest  22505  rnelfmlem  22560  rnelfm  22561  fmfnfmlem2  22563  fmfnfm  22566  lmflf  22613  alexsubALT  22659  clssubg  22717  qustgplem  22729  tsmsres  22752  tsmsxplem1  22761  ucncn  22894  xmettpos  22959  imasdsf1olem  22983  blrnps  23018  blrn  23019  xmeterval  23042  tmslem  23092  tmsxms  23096  imasf1oxms  23099  prdsxms  23140  blval2  23172  metuel2  23175  isngp2  23206  isngp3  23207  tngngp2  23261  isnghm  23332  qtopbaslem  23367  qdensere  23378  cnbl0  23382  cnblcld  23383  cnfldms  23384  blssioo  23403  tgioo  23404  tgqioo  23408  xrtgioo  23414  xrsdsre  23418  xrge0tsms  23442  iimulcn  23542  bndth  23562  lebnumlem3  23567  nmhmcn  23724  cphsqrtcl  23788  lmmbr2  23862  caucfil  23886  causs  23901  lmcau  23916  bcth3  23934  cncms  23958  cnfldcusp  23960  rrxmvallem  24007  ivthicc  24059  ovolfioo  24068  ovolficc  24069  ovolficcss  24070  ovollb2lem  24089  ovoliunlem2  24104  ovolshftlem1  24110  ovolicc2  24123  ismbl  24127  voliunlem2  24152  volsup  24157  ioorf  24174  ioorinv  24177  ioorcl  24178  uniiccdif  24179  uniioovol  24180  uniiccvol  24181  uniioombllem2  24184  uniioombllem4  24187  dyaddisj  24197  dyadmax  24199  dyadmbllem  24200  dyadmbl  24201  opnmbllem  24202  opnmblALT  24204  volsup2  24206  mbfdm  24227  mbfima  24231  mbfid  24236  ismbfd  24240  mbfres2  24246  mbfposr  24253  mbfimaopnlem  24256  mbflimsup  24267  0plef  24273  i1f1lem  24290  itg11  24292  itg1addlem4  24300  i1fpos  24307  itg1le  24314  itg1climres  24315  mbfi1fseqlem5  24320  mbfi1flimlem  24323  xrge0f  24332  itg2ge0  24336  itg2seq  24343  itg2i1fseqle  24355  itg2i1fseq2  24357  itg2addlem  24359  itg2gt0  24361  limciun  24492  dvres  24509  dvres3a  24512  cpnres  24534  dvfre  24548  dvmptres3  24553  dvlip2  24592  dvgt0lem2  24600  deg1fvi  24679  uc1pmon1p  24745  fta1g  24761  ig1peu  24765  ig1pdvds  24770  plyco0  24782  plypf1  24802  dgrlem  24819  dgrub  24824  dgrlb  24826  coemulc  24845  plyreres  24872  plydivlem3  24884  plydivlem4  24885  plydiveu  24887  plyremlem  24893  fta1lem  24896  fta1  24897  vieta1lem2  24900  plyexmo  24902  elaa  24905  elqaalem3  24910  aannenlem1  24917  pserulm  25010  psercnlem2  25012  psercnlem1  25013  psercn  25014  abelth  25029  reeff1o  25035  pilem1  25039  recosf1o  25119  resinf1o  25120  efif1olem3  25128  efif1olem4  25129  efifo  25131  eff1olem  25132  ellogrn  25143  logcn  25230  dvloglem  25231  logf1o2  25233  efopnlem1  25239  efopnlem2  25240  efopn  25241  logtayl  25243  cxpcn3lem  25328  cxpcn3  25329  resqrtcn  25330  asinneg  25464  areambl  25536  emcllem7  25579  lgamgulm2  25613  basellem4  25661  sqff1o  25759  dvdsmulf1o  25771  fsumdvdsmul  25772  ostthlem1  26203  ostth  26215  tglnfn  26333  f1otrg  26657  axlowdimlem6  26733  axlowdimlem8  26735  axlowdimlem9  26736  axlowdimlem11  26738  axlowdimlem12  26739  axlowdimlem17  26744  elntg2  26771  crctcshlem4  27598  clwlkclwwlklem2  27778  eucrct2eupth  28024  ex-fpar  28241  cnnvm  28459  sspmlem  28509  nvo00  28538  nmlno0lem  28570  phoeqi  28634  ubthlem1  28647  hhip  28954  hhssabloilem  29038  hhssnv  29041  hhsssh  29046  occllem  29080  shsel  29091  chscllem2  29415  df0op2  29529  hoeq  29537  hocofni  29544  hoaddfni  29547  hosubfni  29548  hon0  29570  ho01i  29605  hoeq1  29607  elnlfn  29705  nmlnop0iALT  29772  lnopco0i  29781  imaelshi  29835  nlelchi  29838  rnbra  29884  cnvbraval  29887  kbass5  29897  hmopidmchi  29928  hmopidmpji  29929  foresf1o  30265  fimarab  30390  fcomptf  30403  ofpreima  30410  resf1o  30466  maprnin  30467  fpwrelmapffslem  30468  hashgt1  30530  s3clhash  30624  xrge0tsmsd  30692  tocyc01  30760  cyc3evpm  30792  cycpmgcl  30795  cycpmconjslem2  30797  cyc3conja  30799  kerunit  30896  dimval  31001  dimvalfi  31002  txomap  31098  locfinreflem  31104  hauseqcn  31138  xpinpreima  31149  xpinpreima2  31150  tpr2rico  31155  mndpluscn  31169  rmulccn  31171  raddcn  31172  xrge0pluscn  31183  xrge0tmdALT  31189  rge0scvg  31192  pl1cn  31198  elzrhunit  31220  qqhf  31227  cnrrext  31251  qqhre  31261  indpi1  31279  indpreima  31284  1stmbfm  31518  2ndmbfm  31519  mbfmcnt  31526  omssubadd  31558  carsggect  31576  eulerpartlemsv2  31616  eulerpartlems  31618  eulerpartlemv  31622  eulerpartlemb  31626  eulerpartlemf  31628  eulerpartlemt  31629  eulerpartlemmf  31633  eulerpartlemgvv  31634  eulerpartlemgh  31636  eulerpartlemgs2  31638  sseqmw  31649  sseqf  31650  sseqp1  31653  fiblem  31656  fibp1  31659  plymul02  31816  signsvtn0  31840  signstres  31845  signshlen  31860  reprinrn  31889  circlemethhgt  31914  txsconnlem  32487  iccllysconn  32497  rellysconn  32498  cvmseu  32523  cvmliftmolem2  32529  cvmliftlem6  32537  cvmliftlem7  32538  cvmliftlem8  32539  cvmliftlem9  32540  cvmliftlem11  32542  cvmliftlem15  32545  cvmlift2lem7  32556  cvmlift2lem10  32559  cvmlift3lem8  32573  cvmlift3lem9  32574  mvrsfpw  32753  mrsubff1  32761  msrid  32792  msrfo  32793  elmsta  32795  mtyf  32799  msubff1  32803  vhmcls  32813  mclsax  32816  elmthm  32823  mthmblem  32827  mclsppslem  32830  iprodefisumlem  32972  soseq  33096  noetalem3  33219  madeval2  33290  fullfunfnv  33407  fullfunfv  33408  tailfb  33725  filnetlem4  33729  taupilem3  34603  icoreresf  34636  icoreelrnab  34638  relowlssretop  34647  relowlpssretop  34648  unccur  34890  matunitlindflem1  34903  matunitlindflem2  34904  ptrecube  34907  poimirlem28  34935  poimirlem32  34939  heicant  34942  opnmbllem0  34943  mblfinlem1  34944  mblfinlem2  34945  volsupnfl  34952  cnambfre  34955  dvtan  34957  itg2addnclem  34958  itg2addnclem2  34959  ftc1anclem3  34984  ftc1anclem5  34986  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  areacirc  35002  indexdom  35024  sdclem2  35032  sstotbnd2  35067  sstotbnd  35068  isbndx  35075  isbnd3b  35078  prdsbnd  35086  prdstotbnd  35087  ismtyhmeolem  35097  heibor1lem  35102  heiborlem1  35104  heibor  35114  rrnequiv  35128  keridl  35325  ellkr  36240  lkr0f  36245  cdleme50rnlem  37695  elrfirn  39341  ismrcd2  39345  isnacs2  39352  nacsfix  39358  mapfzcons1  39363  mzpcompact2lem  39397  eq0rabdioph  39422  eldioph4b  39457  diophren  39459  pw2f1ocnv  39683  pw2f1o2val2  39686  lmhmfgsplit  39735  pwssplit4  39738  hbt  39779  mpaaeu  39799  mendring  39841  proot1mul  39848  proot1hash  39849  proot1ex  39850  deg1mhm  39856  fgraphopab  39859  hausgraph  39861  ofsubid  40705  expgrowthi  40714  expgrowth  40716  binomcxplemdvbinom  40734  binomcxplemcvg  40735  binomcxplemnotnn0  40737  rfcnpre1  41325  rfcnpre2  41337  cncmpmax  41338  rfcnpre3  41339  rfcnpre4  41340  elixpconstg  41404  ffi  41478  dffo3f  41487  islptre  41949  resincncf  42207  dvcosre  42245  dvresntr  42251  volioof  42321  stoweidlem48  42382  fourierdlem12  42453  fourierdlem15  42456  fourierdlem41  42482  fourierdlem42  42483  fourierdlem46  42486  fourierdlem48  42488  fourierdlem49  42489  fourierdlem54  42494  fourierdlem56  42496  fourierdlem62  42502  fourierdlem64  42504  fourierdlem65  42505  fourierdlem73  42513  fourierdlem74  42514  fourierdlem75  42515  fourierdlem102  42542  fourierdlem103  42543  fourierdlem104  42544  fourierdlem114  42554  sge0split  42740  elhoi  42873  mbfresmf  43065  fafvelrn  43418  ffnafv  43419  fafv2elrn  43482  fafv2elrnb  43483  imarnf1pr  43530  2ffzoeq  43577  fundcmpsurbijinjpreimafv  43616  fundcmpsurinjimaid  43620  fargshiftfv  43648  fargshiftf  43649  fargshiftf1  43650  fargshiftfo  43651  zrinitorngc  44320  zrtermorngc  44321  zrtermoringc  44390  fdmdifeqresdif  44439  fdivmpt  44649  fdivmptf  44650  refdivmptf  44651  aacllem  44951