Theorem ffn 6736

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

Syntax hints:   → wi 4   ⊆ wss 3951  ran crn 5686   Fn wfn 6556  ⟶wf 6557

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 6565

This theorem is referenced by:  ffnd  6737  ffun  6739  frel  6741  fdm  6745  ffrn  6749  fresin  6777  fresaun  6779  fresaunres2  6780  fcoi1  6782  feu  6784  f0bi  6791  dffo2  6824  fimadmfo  6829  fdmeu  6965  feqmptdf  6979  fimarab  6983  fvco3  7008  ffvelcdm  7101  dff2  7119  dffo3  7122  dffo4  7123  dffo5  7124  dffo3f  7126  f1ompt  7131  ffnfv  7139  fcdmssb  7142  fcompt  7153  fsn2  7156  fprb  7214  fconst2g  7223  fpr2g  7231  fex  7246  dff13  7275  nvocnv  7301  soisores  7347  fdmexb  7929  resf1extb  7956  fo1stres  8040  fo2ndres  8041  1stcof  8044  2ndcof  8045  curry1f  8131  curry2f  8133  fparlem1  8137  fparlem2  8138  fo2ndf  8146  soseq  8184  tposf2  8275  smo11  8404  fsetexb  8904  mapsnd  8926  pw2f1olem  9116  mapen  9181  mapunen  9186  fissuni  9397  fipreima  9398  indexfi  9400  mapfien  9448  oismo  9580  cantnflt  9712  cantnfp1lem3  9720  cantnflem4  9732  tcrank  9924  updjudhcoinlf  9972  updjudhcoinrg  9973  updjud  9974  infpwfien  10102  cardinfima  10137  dfacacn  10182  cfflb  10299  cofsmo  10309  cfcoflem  10312  coftr  10313  fin23lem40  10391  axdc3lem2  10491  ac6num  10519  ac6c4  10521  ac6s2  10526  ttukeylem6  10554  iunfo  10579  pwcfsdom  10623  fpwwe2lem5  10675  fpwwe2lem7  10677  pwfseqlem3  10700  inar1  10815  tskcard  10821  tskuni  10823  tskurn  10829  gruima  10842  nqerrel  10972  recmulnq  11004  dmrecnq  11008  axpre-sup  11209  ofsubeq0  12263  dfz2  12632  uzn0  12895  rpnnen1lem3  13021  rpnnen1lem5  13023  unirnioo  13489  dfioo2  13490  ioorebas  13491  fseq1p1m1  13638  2ffzeq  13689  fvinim0ffz  13825  injresinjlem  13826  fsequb2  14017  fseqsupcl  14018  fseqsupubi  14019  ser0f  14096  hashgval  14372  hashinf  14374  hashresfn  14379  ffz0hash  14486  fnfzo0hash  14489  wrdred1hash  14599  revlen  14800  revrev  14805  repswlen  14814  repsdf2  14816  cshword  14829  0csh0  14831  lenco  14871  s1co  14872  cshco  14875  swrdco  14876  s7f1o  15005  ofccat  15008  shftf  15118  uzin2  15383  rexanuz  15384  limsuple  15514  limsupval2  15516  rlimres  15594  lo1res  15595  rlimresb  15601  isercolllem2  15702  isercolllem3  15703  isercoll  15704  supcvg  15892  prodf1f  15928  eff2  16135  reeff1  16156  tanval  16164  ruclem4  16270  ruclem12  16277  prmreclem6  16959  1arithlem4  16964  1arith  16965  vdwmc  17016  vdwlem1  17019  vdwlem8  17026  vdwlem13  17031  ramval  17046  0ram  17058  0ram2  17059  0ramcl  17061  ramcl  17067  fsets  17206  firest  17477  0ssc  17882  0subcat  17883  isfull2  17958  arwhoma  18090  gsumval2a  18698  isgrpinv  19011  kerf1ghm  19265  f1omvdconj  19464  pmtrmvd  19474  pmtrfinv  19479  pmtrdifellem4  19497  efgsfo  19757  efgredlem  19765  efgcpbllemb  19773  frgpup3lem  19795  0frgp  19797  gexex  19871  torsubg  19872  gsumval3  19925  gsumzres  19927  gsummptmhm  19958  gsumzoppg  19962  dprdf1o  20052  dprd2db  20063  zrinitorngc  20642  zrtermorngc  20643  zrtermoringc  20675  srngf1o  20849  lmhmima  21046  lmhmpreima  21047  lmhmrnlss  21049  lspextmo  21055  pwssplit1  21058  cnfldadd  21370  cnfldmul  21372  dfcnfldOLD  21380  cnfldplusf  21409  cnfldsub  21410  chrrhm  21546  znunit  21582  psgnevpmb  21605  psgndiflemB  21618  mpofrlmd  21797  frlmipval  21799  frlmphl  21801  frlmlbs  21817  frlmup4  21821  ellspd  21822  lindfmm  21847  lsslindf  21850  psrbaglefi  21946  psrlidm  21982  mplmonmul  22054  evlseu  22107  mpfconst  22125  mpfproj  22126  mpfsubrg  22127  coe1sclmulfv  22286  pf1const  22350  pf1id  22351  pf1subrg  22352  mpfpf1  22355  pf1mpf  22356  mamuass  22406  mamudi  22407  mamudir  22408  mamuvs1  22409  mamuvs2  22410  1mavmul  22554  mavmulass  22555  mdetunilem7  22624  madutpos  22648  lecldbas  23227  lmbr2  23267  cncnpi  23286  cncnp  23288  cnpdis  23301  lmff  23309  pnrmopn  23351  dnsconst  23386  cmpsub  23408  tgcmp  23409  hauscmplem  23414  2ndcctbss  23463  2ndcomap  23466  2ndcsep  23467  1stccnp  23470  kgenidm  23555  iskgen2  23556  1stckgen  23562  kgen2cn  23567  ptpjpre1  23579  pttop  23590  ptuni  23602  ptval2  23609  tx1cn  23617  tx2cn  23618  ptpjcn  23619  ptpjopn  23620  ptclsg  23623  ptcnplem  23629  upxp  23631  txcnmpt  23632  uptx  23633  txcmplem2  23650  txkgen  23660  xkoptsub  23662  xkopt  23663  xkococnlem  23667  xkococn  23668  ptcmpfi  23821  zfbas  23904  uzrest  23905  rnelfmlem  23960  rnelfm  23961  fmfnfmlem2  23963  fmfnfm  23966  lmflf  24013  alexsubALT  24059  clssubg  24117  qustgplem  24129  tsmsres  24152  tsmsxplem1  24161  ucncn  24294  xmettpos  24359  imasdsf1olem  24383  blrnps  24418  blrn  24419  xmeterval  24442  tmslem  24494  tmslemOLD  24495  tmsxms  24499  imasf1oxms  24502  prdsxms  24543  blval2  24575  metuel2  24578  isngp2  24610  isngp3  24611  tngngp2  24673  isnghm  24744  qtopbaslem  24779  qdensere  24790  cnbl0  24794  cnblcld  24795  cnfldms  24796  blssioo  24816  tgioo  24817  tgqioo  24821  xrtgioo  24828  xrsdsre  24832  xrge0tsms  24856  iimulcnOLD  24968  bndth  24990  lebnumlem3  24995  nmhmcn  25153  cphsqrtcl  25218  lmmbr2  25293  caucfil  25317  causs  25332  lmcau  25347  bcth3  25365  cncms  25389  cnfldcusp  25391  rrxmvallem  25438  ivthicc  25493  ovolfioo  25502  ovolficc  25503  ovolficcss  25504  ovollb2lem  25523  ovoliunlem2  25538  ovolshftlem1  25544  ovolicc2  25557  ismbl  25561  voliunlem2  25586  volsup  25591  ioorf  25608  ioorinv  25611  ioorcl  25612  uniiccdif  25613  uniioovol  25614  uniiccvol  25615  uniioombllem2  25618  uniioombllem4  25621  dyaddisj  25631  dyadmax  25633  dyadmbllem  25634  dyadmbl  25635  opnmbllem  25636  opnmblALT  25638  volsup2  25640  mbfdm  25661  mbfima  25665  mbfid  25670  ismbfd  25674  mbfres2  25680  mbfposr  25687  mbfimaopnlem  25690  mbflimsup  25701  0plef  25707  i1f1lem  25724  itg11  25726  itg1addlem4  25734  i1fpos  25741  itg1le  25748  itg1climres  25749  mbfi1fseqlem5  25754  mbfi1flimlem  25757  xrge0f  25766  itg2ge0  25770  itg2seq  25777  itg2i1fseqle  25789  itg2i1fseq2  25791  itg2addlem  25793  itg2gt0  25795  limciun  25929  dvres  25946  dvres3a  25949  cpnres  25973  dvfre  25989  dvmptres3  25994  dvlip2  26034  dvgt0lem2  26042  deg1fvi  26124  uc1pmon1p  26191  fta1g  26209  ig1peu  26214  ig1pdvds  26219  plyco0  26231  plypf1  26251  dgrlem  26268  dgrub  26273  dgrlb  26275  coemulc  26294  plyreres  26324  plydivlem3  26337  plydivlem4  26338  plydiveu  26340  plyremlem  26346  fta1lem  26349  fta1  26350  vieta1lem2  26353  plyexmo  26355  elaa  26358  elqaalem3  26363  aannenlem1  26370  pserulm  26465  psercnlem2  26468  psercnlem1  26469  psercn  26470  abelth  26485  reeff1o  26491  pilem1  26495  recosf1o  26577  resinf1o  26578  efif1olem3  26586  efif1olem4  26587  efifo  26589  eff1olem  26590  ellogrn  26601  logcn  26689  dvloglem  26690  logf1o2  26692  efopnlem1  26698  efopnlem2  26699  efopn  26700  logtayl  26702  cxpcn3lem  26790  cxpcn3  26791  resqrtcn  26792  asinneg  26929  areambl  27001  emcllem7  27045  lgamgulm2  27079  basellem4  27127  sqff1o  27225  mpodvdsmulf1o  27237  fsumdvdsmul  27238  dvdsmulf1o  27239  fsumdvdsmulOLD  27240  ostthlem1  27671  ostth  27683  noetasuplem4  27781  madeval2  27892  elold  27908  old1  27914  madeoldsuc  27923  tglnfn  28555  f1otrg  28879  axlowdimlem6  28962  axlowdimlem8  28964  axlowdimlem9  28965  axlowdimlem11  28967  axlowdimlem12  28968  axlowdimlem17  28973  elntg2  29000  dfpth2  29749  cyclnumvtx  29820  crctcshlem4  29840  clwlkclwwlklem2  30019  eucrct2eupth  30264  ex-fpar  30481  cnnvm  30701  sspmlem  30751  nvo00  30780  nmlno0lem  30812  phoeqi  30876  ubthlem1  30889  hhip  31196  hhssabloilem  31280  hhssnv  31283  hhsssh  31288  occllem  31322  shsel  31333  chscllem2  31657  df0op2  31771  hoeq  31779  hocofni  31786  hoaddfni  31789  hosubfni  31790  hon0  31812  ho01i  31847  hoeq1  31849  elnlfn  31947  nmlnop0iALT  32014  lnopco0i  32023  imaelshi  32077  nlelchi  32080  rnbra  32126  cnvbraval  32129  kbass5  32139  hmopidmchi  32170  hmopidmpji  32171  foresf1o  32523  fcomptf  32668  ofpreima  32675  resf1o  32741  maprnin  32742  fpwrelmapffslem  32743  hashgt1  32812  indpi1  32845  indpreima  32850  s3clhash  32932  gsumpart  33060  xrge0tsmsd  33065  tocyc01  33138  cyc3evpm  33170  cycpmgcl  33173  cycpmconjslem2  33175  cyc3conja  33177  kerunit  33349  1arithidomlem1  33563  1arithidomlem2  33564  1arithidom  33565  dimval  33651  dimvalfi  33652  ply1degltdimlem  33673  ply1degltdim  33674  elirng  33736  txomap  33833  locfinreflem  33839  hauseqcn  33897  xpinpreima  33905  xpinpreima2  33906  tpr2rico  33911  mndpluscn  33925  raddcn  33928  xrge0pluscn  33939  xrge0tmdALT  33945  rge0scvg  33948  pl1cn  33954  elzrhunit  33978  qqhf  33987  cnrrext  34011  qqhre  34021  1stmbfm  34262  2ndmbfm  34263  mbfmcnt  34270  omssubadd  34302  carsggect  34320  eulerpartlemsv2  34360  eulerpartlems  34362  eulerpartlemv  34366  eulerpartlemb  34370  eulerpartlemf  34372  eulerpartlemt  34373  eulerpartlemmf  34377  eulerpartlemgvv  34378  eulerpartlemgh  34380  eulerpartlemgs2  34382  sseqmw  34393  sseqf  34394  sseqp1  34397  fiblem  34400  fibp1  34403  plymul02  34561  signsvtn0  34585  signstres  34590  signshlen  34605  reprinrn  34633  circlemethhgt  34658  txsconnlem  35245  iccllysconn  35255  rellysconn  35256  cvmseu  35281  cvmliftmolem2  35287  cvmliftlem6  35295  cvmliftlem7  35296  cvmliftlem8  35297  cvmliftlem9  35298  cvmliftlem11  35300  cvmliftlem15  35303  cvmlift2lem7  35314  cvmlift2lem10  35317  cvmlift3lem8  35331  cvmlift3lem9  35332  mvrsfpw  35511  mrsubff1  35519  msrid  35550  msrfo  35551  elmsta  35553  mtyf  35557  msubff1  35561  vhmcls  35571  mclsax  35574  elmthm  35581  mthmblem  35585  mclsppslem  35588  iprodefisumlem  35740  fullfunfnv  35947  fullfunfv  35948  tailfb  36378  filnetlem4  36382  taupilem3  37320  icoreresf  37353  icoreelrnab  37355  relowlssretop  37364  relowlpssretop  37365  unccur  37610  matunitlindflem1  37623  matunitlindflem2  37624  ptrecube  37627  poimirlem28  37655  poimirlem32  37659  heicant  37662  opnmbllem0  37663  mblfinlem1  37664  mblfinlem2  37665  volsupnfl  37672  cnambfre  37675  dvtan  37677  itg2addnclem  37678  itg2addnclem2  37679  ftc1anclem3  37702  ftc1anclem5  37704  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  areacirc  37720  indexdom  37741  sdclem2  37749  sstotbnd2  37781  sstotbnd  37782  isbndx  37789  isbnd3b  37792  prdsbnd  37800  prdstotbnd  37801  ismtyhmeolem  37811  heibor1lem  37816  heiborlem1  37818  heibor  37828  rrnequiv  37842  keridl  38039  ellkr  39090  lkr0f  39095  cdleme50rnlem  40546  aks6d1c2lem4  42128  aks6d1c5  42140  sticksstones11  42157  sticksstones19  42166  sticksstones22  42169  aks6d1c6lem4  42174  aks6d1c6isolem2  42176  fsuppind  42600  elrfirn  42706  ismrcd2  42710  isnacs2  42717  nacsfix  42723  mapfzcons1  42728  mzpcompact2lem  42762  eq0rabdioph  42787  eldioph4b  42822  diophren  42824  pw2f1ocnv  43049  pw2f1o2val2  43052  lmhmfgsplit  43098  pwssplit4  43101  hbt  43142  mpaaeu  43162  mendring  43200  proot1mul  43206  proot1hash  43207  proot1ex  43208  deg1mhm  43212  fgraphopab  43215  hausgraph  43217  nvocnvb  43435  ofsubid  44343  expgrowthi  44352  expgrowth  44354  binomcxplemdvbinom  44372  binomcxplemcvg  44373  binomcxplemnotnn0  44375  relpfrlem  44974  rfcnpre1  45024  rfcnpre2  45036  cncmpmax  45037  rfcnpre3  45038  rfcnpre4  45039  elixpconstg  45094  ffi  45178  islptre  45634  resincncf  45890  dvcosre  45927  dvresntr  45933  volioof  46002  stoweidlem48  46063  fourierdlem12  46134  fourierdlem15  46137  fourierdlem41  46163  fourierdlem42  46164  fourierdlem46  46167  fourierdlem48  46169  fourierdlem49  46170  fourierdlem54  46175  fourierdlem56  46177  fourierdlem62  46183  fourierdlem64  46185  fourierdlem65  46186  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem114  46235  sge0split  46424  elhoi  46557  mbfresmf  46754  cfsetsnfsetf1  47071  cfsetsnfsetfo  47072  focofob  47092  f1ocof1ob  47093  fafvelcdm  47182  ffnafv  47183  fafv2elcdm  47246  fafv2elrnb  47247  imarnf1pr  47294  2ffzoeq  47339  fundcmpsurbijinjpreimafv  47394  fundcmpsurinjimaid  47398  fargshiftfv  47426  fargshiftf  47427  fargshiftf1  47428  fargshiftfo  47429  cycl3grtri  47914  fdmdifeqresdif  48258  fdivmpt  48461  fdivmptf  48462  refdivmptf  48463  1arymaptf1  48563  2arymaptf1  48574  ackfnnn0  48606  aacllem  49320