Theorem ffn 6747

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

Syntax hints:   → wi 4   ⊆ wss 3976  ran crn 5701   Fn wfn 6568  ⟶wf 6569

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 6577

This theorem is referenced by:  ffnd  6748  ffun  6750  frel  6752  fdm  6756  ffrn  6760  fresin  6790  fresaun  6792  fresaunres2  6793  fcoi1  6795  feu  6797  f0bi  6804  dffo2  6838  fimadmfo  6843  fdmeu  6978  feqmptdf  6992  fimarab  6996  fvco3  7021  ffvelcdm  7115  dff2  7133  dffo3  7136  dffo4  7137  dffo5  7138  dffo3f  7140  f1ompt  7145  ffnfv  7153  fcdmssb  7156  fcompt  7167  fsn2  7170  fprb  7231  fconst2g  7240  fpr2g  7248  fex  7263  dff13  7292  nvocnv  7317  soisores  7363  fdmexb  7947  fo1stres  8056  fo2ndres  8057  1stcof  8060  2ndcof  8061  curry1f  8147  curry2f  8149  fparlem1  8153  fparlem2  8154  fo2ndf  8162  soseq  8200  tposf2  8291  smo11  8420  fsetexb  8922  mapsnd  8944  pw2f1olem  9142  mapen  9207  mapunen  9212  fissuni  9427  fipreima  9428  indexfi  9430  mapfien  9477  oismo  9609  cantnflt  9741  cantnfp1lem3  9749  cantnflem4  9761  tcrank  9953  updjudhcoinlf  10001  updjudhcoinrg  10002  updjud  10003  infpwfien  10131  cardinfima  10166  dfacacn  10211  cfflb  10328  cofsmo  10338  cfcoflem  10341  coftr  10342  fin23lem40  10420  axdc3lem2  10520  ac6num  10548  ac6c4  10550  ac6s2  10555  ttukeylem6  10583  iunfo  10608  pwcfsdom  10652  fpwwe2lem5  10704  fpwwe2lem7  10706  pwfseqlem3  10729  inar1  10844  tskcard  10850  tskuni  10852  tskurn  10858  gruima  10871  nqerrel  11001  recmulnq  11033  dmrecnq  11037  axpre-sup  11238  ofsubeq0  12290  dfz2  12658  uzn0  12920  rpnnen1lem3  13044  rpnnen1lem5  13046  unirnioo  13509  dfioo2  13510  ioorebas  13511  fseq1p1m1  13658  2ffzeq  13706  fvinim0ffz  13836  injresinjlem  13837  fsequb2  14027  fseqsupcl  14028  fseqsupubi  14029  ser0f  14106  hashgval  14382  hashinf  14384  hashresfn  14389  ffz0hash  14496  fnfzo0hash  14499  wrdred1hash  14609  revlen  14810  revrev  14815  repswlen  14824  repsdf2  14826  cshword  14839  0csh0  14841  lenco  14881  s1co  14882  cshco  14885  swrdco  14886  s7f1o  15015  ofccat  15018  shftf  15128  uzin2  15393  rexanuz  15394  limsuple  15524  limsupval2  15526  rlimres  15604  lo1res  15605  rlimresb  15611  isercolllem2  15714  isercolllem3  15715  isercoll  15716  supcvg  15904  prodf1f  15940  eff2  16147  reeff1  16168  tanval  16176  ruclem4  16282  ruclem12  16289  prmreclem6  16968  1arithlem4  16973  1arith  16974  vdwmc  17025  vdwlem1  17028  vdwlem8  17035  vdwlem13  17040  ramval  17055  0ram  17067  0ram2  17068  0ramcl  17070  ramcl  17076  fsets  17216  firest  17492  0ssc  17901  0subcat  17902  isfull2  17978  arwhoma  18112  gsumval2a  18723  isgrpinv  19033  kerf1ghm  19287  f1omvdconj  19488  pmtrmvd  19498  pmtrfinv  19503  pmtrdifellem4  19521  efgsfo  19781  efgredlem  19789  efgcpbllemb  19797  frgpup3lem  19819  0frgp  19821  gexex  19895  torsubg  19896  gsumval3  19949  gsumzres  19951  gsummptmhm  19982  gsumzoppg  19986  dprdf1o  20076  dprd2db  20087  zrinitorngc  20664  zrtermorngc  20665  zrtermoringc  20697  srngf1o  20871  lmhmima  21069  lmhmpreima  21070  lmhmrnlss  21072  lspextmo  21078  pwssplit1  21081  cnfldadd  21393  cnfldmul  21395  dfcnfldOLD  21403  cnfldplusf  21432  cnfldsub  21433  chrrhm  21569  znunit  21605  psgnevpmb  21628  psgndiflemB  21641  mpofrlmd  21820  frlmipval  21822  frlmphl  21824  frlmlbs  21840  frlmup4  21844  ellspd  21845  lindfmm  21870  lsslindf  21873  psrbaglefi  21969  psrlidm  22005  mplmonmul  22077  evlseu  22130  mpfconst  22148  mpfproj  22149  mpfsubrg  22150  coe1sclmulfv  22307  pf1const  22371  pf1id  22372  pf1subrg  22373  mpfpf1  22376  pf1mpf  22377  mamuass  22427  mamudi  22428  mamudir  22429  mamuvs1  22430  mamuvs2  22431  1mavmul  22575  mavmulass  22576  mdetunilem7  22645  madutpos  22669  lecldbas  23248  lmbr2  23288  cncnpi  23307  cncnp  23309  cnpdis  23322  lmff  23330  pnrmopn  23372  dnsconst  23407  cmpsub  23429  tgcmp  23430  hauscmplem  23435  2ndcctbss  23484  2ndcomap  23487  2ndcsep  23488  1stccnp  23491  kgenidm  23576  iskgen2  23577  1stckgen  23583  kgen2cn  23588  ptpjpre1  23600  pttop  23611  ptuni  23623  ptval2  23630  tx1cn  23638  tx2cn  23639  ptpjcn  23640  ptpjopn  23641  ptclsg  23644  ptcnplem  23650  upxp  23652  txcnmpt  23653  uptx  23654  txcmplem2  23671  txkgen  23681  xkoptsub  23683  xkopt  23684  xkococnlem  23688  xkococn  23689  ptcmpfi  23842  zfbas  23925  uzrest  23926  rnelfmlem  23981  rnelfm  23982  fmfnfmlem2  23984  fmfnfm  23987  lmflf  24034  alexsubALT  24080  clssubg  24138  qustgplem  24150  tsmsres  24173  tsmsxplem1  24182  ucncn  24315  xmettpos  24380  imasdsf1olem  24404  blrnps  24439  blrn  24440  xmeterval  24463  tmslem  24515  tmslemOLD  24516  tmsxms  24520  imasf1oxms  24523  prdsxms  24564  blval2  24596  metuel2  24599  isngp2  24631  isngp3  24632  tngngp2  24694  isnghm  24765  qtopbaslem  24800  qdensere  24811  cnbl0  24815  cnblcld  24816  cnfldms  24817  blssioo  24836  tgioo  24837  tgqioo  24841  xrtgioo  24847  xrsdsre  24851  xrge0tsms  24875  iimulcnOLD  24987  bndth  25009  lebnumlem3  25014  nmhmcn  25172  cphsqrtcl  25237  lmmbr2  25312  caucfil  25336  causs  25351  lmcau  25366  bcth3  25384  cncms  25408  cnfldcusp  25410  rrxmvallem  25457  ivthicc  25512  ovolfioo  25521  ovolficc  25522  ovolficcss  25523  ovollb2lem  25542  ovoliunlem2  25557  ovolshftlem1  25563  ovolicc2  25576  ismbl  25580  voliunlem2  25605  volsup  25610  ioorf  25627  ioorinv  25630  ioorcl  25631  uniiccdif  25632  uniioovol  25633  uniiccvol  25634  uniioombllem2  25637  uniioombllem4  25640  dyaddisj  25650  dyadmax  25652  dyadmbllem  25653  dyadmbl  25654  opnmbllem  25655  opnmblALT  25657  volsup2  25659  mbfdm  25680  mbfima  25684  mbfid  25689  ismbfd  25693  mbfres2  25699  mbfposr  25706  mbfimaopnlem  25709  mbflimsup  25720  0plef  25726  i1f1lem  25743  itg11  25745  itg1addlem4  25753  itg1addlem4OLD  25754  i1fpos  25761  itg1le  25768  itg1climres  25769  mbfi1fseqlem5  25774  mbfi1flimlem  25777  xrge0f  25786  itg2ge0  25790  itg2seq  25797  itg2i1fseqle  25809  itg2i1fseq2  25811  itg2addlem  25813  itg2gt0  25815  limciun  25949  dvres  25966  dvres3a  25969  cpnres  25993  dvfre  26009  dvmptres3  26014  dvlip2  26054  dvgt0lem2  26062  deg1fvi  26144  uc1pmon1p  26211  fta1g  26229  ig1peu  26234  ig1pdvds  26239  plyco0  26251  plypf1  26271  dgrlem  26288  dgrub  26293  dgrlb  26295  coemulc  26314  plyreres  26342  plydivlem3  26355  plydivlem4  26356  plydiveu  26358  plyremlem  26364  fta1lem  26367  fta1  26368  vieta1lem2  26371  plyexmo  26373  elaa  26376  elqaalem3  26381  aannenlem1  26388  pserulm  26483  psercnlem2  26486  psercnlem1  26487  psercn  26488  abelth  26503  reeff1o  26509  pilem1  26513  recosf1o  26595  resinf1o  26596  efif1olem3  26604  efif1olem4  26605  efifo  26607  eff1olem  26608  ellogrn  26619  logcn  26707  dvloglem  26708  logf1o2  26710  efopnlem1  26716  efopnlem2  26717  efopn  26718  logtayl  26720  cxpcn3lem  26808  cxpcn3  26809  resqrtcn  26810  asinneg  26947  areambl  27019  emcllem7  27063  lgamgulm2  27097  basellem4  27145  sqff1o  27243  mpodvdsmulf1o  27255  fsumdvdsmul  27256  dvdsmulf1o  27257  fsumdvdsmulOLD  27258  ostthlem1  27689  ostth  27701  noetasuplem4  27799  madeval2  27910  elold  27926  old1  27932  madeoldsuc  27941  tglnfn  28573  f1otrg  28897  axlowdimlem6  28980  axlowdimlem8  28982  axlowdimlem9  28983  axlowdimlem11  28985  axlowdimlem12  28986  axlowdimlem17  28991  elntg2  29018  crctcshlem4  29853  clwlkclwwlklem2  30032  eucrct2eupth  30277  ex-fpar  30494  cnnvm  30714  sspmlem  30764  nvo00  30793  nmlno0lem  30825  phoeqi  30889  ubthlem1  30902  hhip  31209  hhssabloilem  31293  hhssnv  31296  hhsssh  31301  occllem  31335  shsel  31346  chscllem2  31670  df0op2  31784  hoeq  31792  hocofni  31799  hoaddfni  31802  hosubfni  31803  hon0  31825  ho01i  31860  hoeq1  31862  elnlfn  31960  nmlnop0iALT  32027  lnopco0i  32036  imaelshi  32090  nlelchi  32093  rnbra  32139  cnvbraval  32142  kbass5  32152  hmopidmchi  32183  hmopidmpji  32184  foresf1o  32532  fcomptf  32676  ofpreima  32683  resf1o  32744  maprnin  32745  fpwrelmapffslem  32746  hashgt1  32815  s3clhash  32914  gsumpart  33038  xrge0tsmsd  33041  tocyc01  33111  cyc3evpm  33143  cycpmgcl  33146  cycpmconjslem2  33148  cyc3conja  33150  kerunit  33314  1arithidomlem1  33528  1arithidomlem2  33529  1arithidom  33530  dimval  33613  dimvalfi  33614  ply1degltdimlem  33635  ply1degltdim  33636  elirng  33686  txomap  33780  locfinreflem  33786  hauseqcn  33844  xpinpreima  33852  xpinpreima2  33853  tpr2rico  33858  mndpluscn  33872  raddcn  33875  xrge0pluscn  33886  xrge0tmdALT  33892  rge0scvg  33895  pl1cn  33901  elzrhunit  33925  qqhf  33932  cnrrext  33956  qqhre  33966  indpi1  33984  indpreima  33989  1stmbfm  34225  2ndmbfm  34226  mbfmcnt  34233  omssubadd  34265  carsggect  34283  eulerpartlemsv2  34323  eulerpartlems  34325  eulerpartlemv  34329  eulerpartlemb  34333  eulerpartlemf  34335  eulerpartlemt  34336  eulerpartlemmf  34340  eulerpartlemgvv  34341  eulerpartlemgh  34343  eulerpartlemgs2  34345  sseqmw  34356  sseqf  34357  sseqp1  34360  fiblem  34363  fibp1  34366  plymul02  34523  signsvtn0  34547  signstres  34552  signshlen  34567  reprinrn  34595  circlemethhgt  34620  txsconnlem  35208  iccllysconn  35218  rellysconn  35219  cvmseu  35244  cvmliftmolem2  35250  cvmliftlem6  35258  cvmliftlem7  35259  cvmliftlem8  35260  cvmliftlem9  35261  cvmliftlem11  35263  cvmliftlem15  35266  cvmlift2lem7  35277  cvmlift2lem10  35280  cvmlift3lem8  35294  cvmlift3lem9  35295  mvrsfpw  35474  mrsubff1  35482  msrid  35513  msrfo  35514  elmsta  35516  mtyf  35520  msubff1  35524  vhmcls  35534  mclsax  35537  elmthm  35544  mthmblem  35548  mclsppslem  35551  iprodefisumlem  35702  fullfunfnv  35910  fullfunfv  35911  tailfb  36343  filnetlem4  36347  taupilem3  37285  icoreresf  37318  icoreelrnab  37320  relowlssretop  37329  relowlpssretop  37330  unccur  37563  matunitlindflem1  37576  matunitlindflem2  37577  ptrecube  37580  poimirlem28  37608  poimirlem32  37612  heicant  37615  opnmbllem0  37616  mblfinlem1  37617  mblfinlem2  37618  volsupnfl  37625  cnambfre  37628  dvtan  37630  itg2addnclem  37631  itg2addnclem2  37632  ftc1anclem3  37655  ftc1anclem5  37657  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  areacirc  37673  indexdom  37694  sdclem2  37702  sstotbnd2  37734  sstotbnd  37735  isbndx  37742  isbnd3b  37745  prdsbnd  37753  prdstotbnd  37754  ismtyhmeolem  37764  heibor1lem  37769  heiborlem1  37771  heibor  37781  rrnequiv  37795  keridl  37992  ellkr  39045  lkr0f  39050  cdleme50rnlem  40501  aks6d1c2lem4  42084  aks6d1c5  42096  sticksstones11  42113  sticksstones19  42122  sticksstones22  42125  aks6d1c6lem4  42130  aks6d1c6isolem2  42132  fsuppind  42545  elrfirn  42651  ismrcd2  42655  isnacs2  42662  nacsfix  42668  mapfzcons1  42673  mzpcompact2lem  42707  eq0rabdioph  42732  eldioph4b  42767  diophren  42769  pw2f1ocnv  42994  pw2f1o2val2  42997  lmhmfgsplit  43043  pwssplit4  43046  hbt  43087  mpaaeu  43107  mendring  43149  proot1mul  43155  proot1hash  43156  proot1ex  43157  deg1mhm  43161  fgraphopab  43164  hausgraph  43166  nvocnvb  43384  ofsubid  44293  expgrowthi  44302  expgrowth  44304  binomcxplemdvbinom  44322  binomcxplemcvg  44323  binomcxplemnotnn0  44325  rfcnpre1  44919  rfcnpre2  44931  cncmpmax  44932  rfcnpre3  44933  rfcnpre4  44934  elixpconstg  44991  ffi  45080  islptre  45540  resincncf  45796  dvcosre  45833  dvresntr  45839  volioof  45908  stoweidlem48  45969  fourierdlem12  46040  fourierdlem15  46043  fourierdlem41  46069  fourierdlem42  46070  fourierdlem46  46073  fourierdlem48  46075  fourierdlem49  46076  fourierdlem54  46081  fourierdlem56  46083  fourierdlem62  46089  fourierdlem64  46091  fourierdlem65  46092  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem102  46129  fourierdlem103  46130  fourierdlem104  46131  fourierdlem114  46141  sge0split  46330  elhoi  46463  mbfresmf  46660  cfsetsnfsetf1  46974  cfsetsnfsetfo  46975  focofob  46995  f1ocof1ob  46996  fafvelcdm  47085  ffnafv  47086  fafv2elcdm  47149  fafv2elrnb  47150  imarnf1pr  47197  2ffzoeq  47242  fundcmpsurbijinjpreimafv  47281  fundcmpsurinjimaid  47285  fargshiftfv  47313  fargshiftf  47314  fargshiftf1  47315  fargshiftfo  47316  fdmdifeqresdif  48066  fdivmpt  48274  fdivmptf  48275  refdivmptf  48276  1arymaptf1  48376  2arymaptf1  48387  ackfnnn0  48419  aacllem  48895