Theorem ffn 6705

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

Syntax hints:   → wi 4   ⊆ wss 3905  ran crn 5662   Fn wfn 6531  ⟶wf 6532

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 210  df-an 401  df-f 6540

This theorem is referenced by:  ffnd  6706  ffun  6708  ffunOLD  6709  frel  6711  fdm  6715  ffrn  6719  fresin  6747  fresaun  6749  fresaunres2  6750  fcoi1  6752  feu  6754  f0bi  6761  dffo2  6796  fimadmfo  6801  fdmeu  6937  feqmptdf  6951  fimarab  6955  fvco3  6981  ffvelcdm  7076  dff2  7094  dffo3  7097  dffo4  7098  dffo5  7099  dffo3f  7101  f1ompt  7106  ffnfv  7114  fcdmssb  7117  fcompt  7129  fsn2  7132  fprb  7192  fconst2g  7201  fpr2g  7209  fex  7224  dff13  7252  nvocnv  7279  soisores  7325  fdmexb  7900  resf1extb  7927  fo1stres  8008  fo2ndres  8009  1stcof  8012  2ndcof  8013  curry1f  8097  curry2f  8099  fparlem1  8103  fparlem2  8104  fo2ndf  8112  soseq  8151  tposf2  8242  smo11  8347  fsetexb  8857  mapsnd  8880  pw2f1olem  9065  mapen  9125  mapunen  9130  fissuni  9310  fipreima  9311  indexfi  9313  mapfien  9364  oismo  9498  cantnflt  9637  cantnfp1lem3  9645  cantnflem4  9657  tcrank  9852  updjudhcoinlf  9914  updjudhcoinrg  9915  updjud  9916  infpwfien  10042  cardinfima  10077  dfacacn  10121  cfflb  10238  cofsmo  10248  cfcoflem  10251  coftr  10252  fin23lem40  10330  axdc3lem2  10430  ac6num  10458  ac6c4  10460  ac6s2  10465  ttukeylem6  10493  iunfo  10518  pwcfsdom  10563  fpwwe2lem5  10615  fpwwe2lem7  10617  pwfseqlem3  10640  inar1  10755  tskcard  10761  tskuni  10763  tskurn  10769  gruima  10782  nqerrel  10912  recmulnq  10944  dmrecnq  10948  axpre-sup  11149  ofsubeq0  12210  indpi1  12227  dfz2  12605  uzn0  12874  rpnnen1lem3  12998  rpnnen1lem5  13000  unirnioo  13471  dfioo2  13472  ioorebas  13473  fseq1p1m1  13622  2ffzeq  13673  fvinim0ffz  13814  injresinjlem  13815  fsequb2  14008  fseqsupcl  14009  fseqsupubi  14010  ser0f  14087  hashgval  14365  hashinf  14367  hashresfn  14372  ffz0hash  14480  fnfzo0hash  14483  wrdred1hash  14594  revlen  14795  revrev  14800  repswlen  14809  repsdf2  14811  cshword  14824  0csh0  14826  lenco  14865  s1co  14866  cshco  14869  swrdco  14870  s7f1o  14999  ofccat  15002  shftf  15112  uzin2  15392  rexanuz  15393  limsuple  15525  limsupval2  15527  rlimres  15605  lo1res  15606  rlimresb  15612  isercolllem2  15713  isercolllem3  15714  isercoll  15715  supcvg  15906  prodf1f  15942  eff2  16150  reeff1  16171  tanval  16179  ruclem4  16285  ruclem12  16292  prmreclem6  16976  1arithlem4  16981  1arith  16982  vdwmc  17033  vdwlem1  17036  vdwlem8  17043  vdwlem13  17048  ramval  17063  0ram  17075  0ram2  17076  0ramcl  17078  ramcl  17084  fsets  17224  firest  17480  0ssc  17889  0subcat  17890  isfull2  17965  arwhoma  18097  gsumval2a  18738  isgrpinv  19055  kerf1ghm  19312  f1omvdconj  19511  pmtrmvd  19521  pmtrfinv  19526  pmtrdifellem4  19544  efgsfo  19804  efgredlem  19812  efgcpbllemb  19820  frgpup3lem  19842  0frgp  19844  gexex  19918  torsubg  19919  gsumval3  19972  gsumzres  19974  gsummptmhm  20005  gsumzoppg  20009  dprdf1o  20099  dprd2db  20110  zrinitorngc  20741  zrtermorngc  20742  zrtermoringc  20774  srngf1o  20951  lmhmima  21168  lmhmpreima  21169  lmhmrnlss  21171  lspextmo  21177  pwssplit1  21180  cnfldadd  21528  cnfldmul  21530  cnfldplusf  21549  cnfldsub  21550  chrrhm  21681  znunit  21713  psgnevpmb  21737  psgndiflemB  21750  mpofrlmd  21927  frlmipval  21929  frlmphl  21931  frlmlbs  21947  frlmup4  21951  ellspd  21952  lindfmm  21977  lsslindf  21980  psrbaglefi  22076  psrlidm  22111  mplmonmul  22187  evlseu  22234  mpfconst  22260  mpfproj  22261  mpfsubrg  22262  coe1sclmulfv  22444  pf1const  22506  pf1id  22507  pf1subrg  22508  mpfpf1  22511  pf1mpf  22512  mamuass  22559  mamudi  22560  mamudir  22561  mamuvs1  22562  mamuvs2  22563  1mavmul  22705  mavmulass  22706  mdetunilem7  22775  madutpos  22799  lecldbas  23376  lmbr2  23416  cncnpi  23435  cncnp  23437  cnpdis  23450  lmff  23458  pnrmopn  23500  dnsconst  23535  cmpsub  23557  tgcmp  23558  hauscmplem  23563  2ndcctbss  23612  2ndcomap  23615  2ndcsep  23616  1stccnp  23619  kgenidm  23704  iskgen2  23705  1stckgen  23711  kgen2cn  23716  ptpjpre1  23728  pttop  23739  ptuni  23751  ptval2  23758  tx1cn  23766  tx2cn  23767  ptpjcn  23768  ptpjopn  23769  ptclsg  23772  ptcnplem  23778  upxp  23780  txcnmpt  23781  uptx  23782  txcmplem2  23799  txkgen  23809  xkoptsub  23811  xkopt  23812  xkococnlem  23816  xkococn  23817  ptcmpfi  23970  zfbas  24053  uzrest  24054  rnelfmlem  24109  rnelfm  24110  fmfnfmlem2  24112  fmfnfm  24115  lmflf  24162  alexsubALT  24208  clssubg  24266  qustgplem  24278  tsmsres  24301  tsmsxplem1  24310  ucncn  24441  xmettpos  24506  imasdsf1olem  24530  blrnps  24565  blrn  24566  xmeterval  24589  tmslem  24639  tmsxms  24643  imasf1oxms  24646  prdsxms  24687  blval2  24719  metuel2  24722  isngp2  24754  isngp3  24755  tngngp2  24809  isnghm  24880  qtopbaslem  24915  qdensere  24926  cnbl0  24930  cnblcld  24931  cnfldms  24932  blssioo  24952  tgioo  24953  tgqioo  24957  xrtgioo  24964  xrsdsre  24968  xrge0tsms  24992  bndth  25117  lebnumlem3  25122  nmhmcn  25279  cphsqrtcl  25343  lmmbr2  25418  caucfil  25442  causs  25457  lmcau  25472  bcth3  25490  cncms  25514  cnfldcusp  25516  rrxmvallem  25563  ivthicc  25617  ovolfioo  25626  ovolficc  25627  ovolficcss  25628  ovollb2lem  25647  ovoliunlem2  25662  ovolshftlem1  25668  ovolicc2  25681  ismbl  25685  voliunlem2  25710  volsup  25715  ioorf  25732  ioorinv  25735  ioorcl  25736  uniiccdif  25737  uniioovol  25738  uniiccvol  25739  uniioombllem2  25742  uniioombllem4  25745  dyaddisj  25755  dyadmax  25757  dyadmbllem  25758  dyadmbl  25759  opnmbllem  25760  opnmblALT  25762  volsup2  25764  mbfdm  25785  mbfima  25789  mbfid  25794  ismbfd  25798  mbfres2  25804  mbfposr  25811  mbfimaopnlem  25814  mbflimsup  25825  0plef  25831  i1f1lem  25848  itg11  25850  itg1addlem4  25858  i1fpos  25865  itg1le  25872  itg1climres  25873  mbfi1fseqlem5  25878  mbfi1flimlem  25881  xrge0f  25890  itg2ge0  25894  itg2seq  25901  itg2i1fseqle  25913  itg2i1fseq2  25915  itg2addlem  25917  itg2gt0  25919  limciun  26053  dvres  26070  dvres3a  26073  cpnres  26096  dvfre  26110  dvmptres3  26115  dvlip2  26154  dvgt0lem2  26162  deg1fvi  26242  uc1pmon1p  26309  fta1g  26327  ig1peu  26332  ig1pdvds  26337  plyco0  26349  plypf1  26369  dgrlem  26386  dgrub  26391  dgrlb  26393  coemulc  26412  plymul02  26441  plyreres  26444  plydivlem3  26456  plydivlem4  26457  plydiveu  26459  plyremlem  26465  fta1lem  26468  fta1  26469  vieta1lem2  26472  plyexmo  26474  elaa  26477  elqaalem3  26482  aannenlem1  26491  pserulm  26585  psercnlem2  26587  psercnlem1  26588  psercn  26589  abelth  26604  reeff1o  26610  pilem1  26614  recosf1o  26700  resinf1o  26701  efif1olem3  26709  efif1olem4  26710  efifo  26712  eff1olem  26713  ellogrn  26724  logcn  26812  dvloglem  26813  logf1o2  26815  efopnlem1  26821  efopnlem2  26822  efopn  26823  logtayl  26825  cxpcn3lem  26912  cxpcn3  26913  resqrtcn  26914  asinneg  27051  areambl  27123  emcllem7  27166  lgamgulm2  27200  basellem4  27248  sqff1o  27346  mpodvdsmulf1o  27358  fsumdvdsmul  27359  dvdsmulf1o  27360  ostthlem1  27791  ostth  27803  noetasuplem4  27900  madeval2  28026  elold  28052  old1  28058  madeoldsuc  28078  tglnfn  28816  tgplnfn  29057  f1otrg  29220  axlowdimlem6  29297  axlowdimlem8  29299  axlowdimlem9  29300  axlowdimlem11  29302  axlowdimlem12  29303  axlowdimlem17  29308  elntg2  29335  dfpth2  30078  cyclnumvtx  30149  crctcshlem4  30169  clwlkclwwlklem2  30351  eucrct2eupth  30596  ex-fpar  30813  cnnvm  31034  sspmlem  31084  nvo00  31113  nmlno0lem  31145  phoeqi  31209  ubthlem1  31222  hhip  31529  hhssabloilem  31613  hhssnv  31616  hhsssh  31621  occllem  31655  shsel  31666  chscllem2  31990  df0op2  32104  hoeq  32112  hocofni  32119  hoaddfni  32122  hosubfni  32123  hon0  32145  ho01i  32180  hoeq1  32182  elnlfn  32280  nmlnop0iALT  32347  lnopco0i  32356  imaelshi  32410  nlelchi  32413  rnbra  32459  cnvbraval  32462  kbass5  32472  hmopidmchi  32503  hmopidmpji  32504  foresf1o  32850  fcomptf  33003  ofpreima  33010  resf1o  33075  maprnin  33076  fpwrelmapffslem  33077  hashgt1  33153  indpreima  33185  s3clhash  33268  gsumpart  33383  xrge0tsmsd  33393  tocyc01  33438  cyc3evpm  33470  cycpmgcl  33473  cycpmconjslem2  33475  cyc3conja  33477  kerunit  33645  1arithidomlem1  33825  1arithidomlem2  33826  1arithidom  33827  psrmonmul  33940  dimval  33991  dimvalfi  33992  ply1degltdimlem  34012  ply1degltdim  34013  elirng  34076  txomap  34224  locfinreflem  34230  hauseqcn  34288  xpinpreima  34296  xpinpreima2  34297  tpr2rico  34302  mndpluscn  34316  raddcn  34319  xrge0pluscn  34330  xrge0tmdALT  34336  rge0scvg  34339  pl1cn  34345  elzrhunit  34367  qqhf  34376  cnrrext  34400  qqhre  34410  1stmbfm  34650  2ndmbfm  34651  mbfmcnt  34658  omssubadd  34690  carsggect  34708  eulerpartlemsv2  34748  eulerpartlems  34750  eulerpartlemv  34754  eulerpartlemb  34758  eulerpartlemf  34760  eulerpartlemt  34761  eulerpartlemmf  34765  eulerpartlemgvv  34766  eulerpartlemgh  34768  eulerpartlemgs2  34770  sseqmw  34781  sseqf  34782  sseqp1  34785  fiblem  34788  fibp1  34791  signsvtn0  34957  signstres  34962  signshlen  34977  reprinrn  35005  circlemethhgt  35030  txsconnlem  35732  iccllysconn  35742  rellysconn  35743  cvmseu  35768  cvmliftmolem2  35774  cvmliftlem6  35782  cvmliftlem7  35783  cvmliftlem8  35784  cvmliftlem9  35785  cvmliftlem11  35787  cvmliftlem15  35790  cvmlift2lem7  35801  cvmlift2lem10  35804  cvmlift3lem8  35818  cvmlift3lem9  35819  mvrsfpw  35998  mrsubff1  36006  msrid  36037  msrfo  36038  elmsta  36040  mtyf  36044  msubff1  36048  vhmcls  36058  mclsax  36061  elmthm  36068  mthmblem  36072  mclsppslem  36075  iprodefisumlem  36232  fullfunfnv  36438  fullfunfv  36439  tailfb  36888  filnetlem4  36892  regsfromunir1  37051  taupilem3  37963  icoreresf  37998  icoreelrnab  38000  relowlssretop  38009  relowlpssretop  38010  unccur  38254  matunitlindflem1  38267  matunitlindflem2  38268  ptrecube  38271  poimirlem28  38299  poimirlem32  38303  heicant  38306  opnmbllem0  38307  mblfinlem1  38308  mblfinlem2  38309  volsupnfl  38316  cnambfre  38319  dvtan  38321  itg2addnclem  38322  itg2addnclem2  38323  ftc1anclem3  38346  ftc1anclem5  38348  ftc1anclem7  38350  ftc1anclem8  38351  ftc1anc  38352  areacirc  38364  indexdom  38385  sdclem2  38393  sstotbnd2  38425  sstotbnd  38426  isbndx  38433  isbnd3b  38436  prdsbnd  38444  prdstotbnd  38445  ismtyhmeolem  38455  heibor1lem  38460  heiborlem1  38462  heibor  38472  rrnequiv  38486  keridl  38683  ellkr  39863  lkr0f  39868  cdleme50rnlem  41318  aks6d1c2lem4  42894  aks6d1c5  42906  sticksstones11  42923  sticksstones19  42932  sticksstones22  42935  aks6d1c6lem4  42940  aks6d1c6isolem2  42942  fsuppind  43322  elrfirn  43426  ismrcd2  43430  isnacs2  43437  nacsfix  43443  mapfzcons1  43448  mzpcompact2lem  43482  eq0rabdioph  43507  eldioph4b  43538  diophren  43540  pw2f1ocnv  43764  pw2f1o2val2  43767  lmhmfgsplit  43813  pwssplit4  43816  hbt  43857  mpaaeu  43877  mendring  43915  proot1mul  43921  proot1hash  43922  proot1ex  43923  deg1mhm  43927  fgraphopab  43930  hausgraph  43932  nvocnvb  44148  ofsubid  45034  expgrowthi  45043  expgrowth  45045  binomcxplemdvbinom  45063  binomcxplemcvg  45064  binomcxplemnotnn0  45066  relpfrlem  45662  rfcnpre1  45739  rfcnpre2  45751  cncmpmax  45752  rfcnpre3  45753  rfcnpre4  45754  elixpconstg  45807  ffi  45891  islptre  46335  resincncf  46589  dvcosre  46626  dvresntr  46632  volioof  46701  stoweidlem48  46762  fourierdlem12  46833  fourierdlem15  46836  fourierdlem41  46862  fourierdlem42  46863  fourierdlem46  46866  fourierdlem54  46874  fourierdlem56  46876  fourierdlem62  46882  fourierdlem64  46884  fourierdlem65  46885  fourierdlem73  46893  fourierdlem74  46894  fourierdlem75  46895  fourierdlem102  46922  fourierdlem103  46923  fourierdlem104  46924  fourierdlem114  46934  sge0split  47123  elhoi  47256  mbfresmf  47453  cjnpoly  47626  cfsetsnfsetf1  47796  cfsetsnfsetfo  47797  focofob  47817  f1ocof1ob  47818  fafvelcdm  47907  ffnafv  47908  fafv2elcdm  47971  fafv2elrnb  47972  imarnf1pr  48019  2ffzoeq  48065  fundcmpsurbijinjpreimafv  48156  fundcmpsurinjimaid  48160  fargshiftfv  48188  fargshiftf  48189  fargshiftf1  48190  fargshiftfo  48191  cycl3grtri  48712  fdmdifeqresdif  49122  fdivmpt  49320  fdivmptf  49321  refdivmptf  49322  1arymaptf1  49422  2arymaptf1  49433  ackfnnn0  49465  homf0  49787  aacllem  50621