Theorem ffn 6646

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

Syntax hints:   → wi 4   ⊆ wss 3897  ran crn 5612   Fn wfn 6471  ⟶wf 6472

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 6480

This theorem is referenced by:  ffnd  6647  ffun  6649  frel  6651  fdm  6655  ffrn  6659  fresin  6687  fresaun  6689  fresaunres2  6690  fcoi1  6692  feu  6694  f0bi  6701  dffo2  6734  fimadmfo  6739  fdmeu  6873  feqmptdf  6887  fimarab  6891  fvco3  6916  ffvelcdm  7009  dff2  7027  dffo3  7030  dffo4  7031  dffo5  7032  dffo3f  7034  f1ompt  7039  ffnfv  7047  fcdmssb  7050  fcompt  7061  fsn2  7064  fprb  7123  fconst2g  7132  fpr2g  7140  fex  7155  dff13  7183  nvocnv  7210  soisores  7256  fdmexb  7832  resf1extb  7859  fo1stres  7942  fo2ndres  7943  1stcof  7946  2ndcof  7947  curry1f  8031  curry2f  8033  fparlem1  8037  fparlem2  8038  fo2ndf  8046  soseq  8084  tposf2  8175  smo11  8279  fsetexb  8783  mapsnd  8805  pw2f1olem  8989  mapen  9049  mapunen  9054  fissuni  9236  fipreima  9237  indexfi  9239  mapfien  9287  oismo  9421  cantnflt  9557  cantnfp1lem3  9565  cantnflem4  9577  tcrank  9772  updjudhcoinlf  9820  updjudhcoinrg  9821  updjud  9822  infpwfien  9948  cardinfima  9983  dfacacn  10028  cfflb  10145  cofsmo  10155  cfcoflem  10158  coftr  10159  fin23lem40  10237  axdc3lem2  10337  ac6num  10365  ac6c4  10367  ac6s2  10372  ttukeylem6  10400  iunfo  10425  pwcfsdom  10469  fpwwe2lem5  10521  fpwwe2lem7  10523  pwfseqlem3  10546  inar1  10661  tskcard  10667  tskuni  10669  tskurn  10675  gruima  10688  nqerrel  10818  recmulnq  10850  dmrecnq  10854  axpre-sup  11055  ofsubeq0  12117  dfz2  12482  uzn0  12744  rpnnen1lem3  12872  rpnnen1lem5  12874  unirnioo  13344  dfioo2  13345  ioorebas  13346  fseq1p1m1  13493  2ffzeq  13544  fvinim0ffz  13684  injresinjlem  13685  fsequb2  13878  fseqsupcl  13879  fseqsupubi  13880  ser0f  13957  hashgval  14235  hashinf  14237  hashresfn  14242  ffz0hash  14349  fnfzo0hash  14352  wrdred1hash  14463  revlen  14664  revrev  14669  repswlen  14678  repsdf2  14680  cshword  14693  0csh0  14695  lenco  14734  s1co  14735  cshco  14738  swrdco  14739  s7f1o  14868  ofccat  14871  shftf  14981  uzin2  15247  rexanuz  15248  limsuple  15380  limsupval2  15382  rlimres  15460  lo1res  15461  rlimresb  15467  isercolllem2  15568  isercolllem3  15569  isercoll  15570  supcvg  15758  prodf1f  15794  eff2  16003  reeff1  16024  tanval  16032  ruclem4  16138  ruclem12  16145  prmreclem6  16828  1arithlem4  16833  1arith  16834  vdwmc  16885  vdwlem1  16888  vdwlem8  16895  vdwlem13  16900  ramval  16915  0ram  16927  0ram2  16928  0ramcl  16930  ramcl  16936  fsets  17075  firest  17331  0ssc  17739  0subcat  17740  isfull2  17815  arwhoma  17947  gsumval2a  18588  isgrpinv  18901  kerf1ghm  19154  f1omvdconj  19353  pmtrmvd  19363  pmtrfinv  19368  pmtrdifellem4  19386  efgsfo  19646  efgredlem  19654  efgcpbllemb  19662  frgpup3lem  19684  0frgp  19686  gexex  19760  torsubg  19761  gsumval3  19814  gsumzres  19816  gsummptmhm  19847  gsumzoppg  19851  dprdf1o  19941  dprd2db  19952  zrinitorngc  20552  zrtermorngc  20553  zrtermoringc  20585  srngf1o  20758  lmhmima  20976  lmhmpreima  20977  lmhmrnlss  20979  lspextmo  20985  pwssplit1  20988  cnfldadd  21292  cnfldmul  21294  dfcnfldOLD  21302  cnfldplusf  21328  cnfldsub  21329  chrrhm  21463  znunit  21495  psgnevpmb  21519  psgndiflemB  21532  mpofrlmd  21709  frlmipval  21711  frlmphl  21713  frlmlbs  21729  frlmup4  21733  ellspd  21734  lindfmm  21759  lsslindf  21762  psrbaglefi  21858  psrlidm  21894  mplmonmul  21966  evlseu  22013  mpfconst  22031  mpfproj  22032  mpfsubrg  22033  coe1sclmulfv  22192  pf1const  22256  pf1id  22257  pf1subrg  22258  mpfpf1  22261  pf1mpf  22262  mamuass  22312  mamudi  22313  mamudir  22314  mamuvs1  22315  mamuvs2  22316  1mavmul  22458  mavmulass  22459  mdetunilem7  22528  madutpos  22552  lecldbas  23129  lmbr2  23169  cncnpi  23188  cncnp  23190  cnpdis  23203  lmff  23211  pnrmopn  23253  dnsconst  23288  cmpsub  23310  tgcmp  23311  hauscmplem  23316  2ndcctbss  23365  2ndcomap  23368  2ndcsep  23369  1stccnp  23372  kgenidm  23457  iskgen2  23458  1stckgen  23464  kgen2cn  23469  ptpjpre1  23481  pttop  23492  ptuni  23504  ptval2  23511  tx1cn  23519  tx2cn  23520  ptpjcn  23521  ptpjopn  23522  ptclsg  23525  ptcnplem  23531  upxp  23533  txcnmpt  23534  uptx  23535  txcmplem2  23552  txkgen  23562  xkoptsub  23564  xkopt  23565  xkococnlem  23569  xkococn  23570  ptcmpfi  23723  zfbas  23806  uzrest  23807  rnelfmlem  23862  rnelfm  23863  fmfnfmlem2  23865  fmfnfm  23868  lmflf  23915  alexsubALT  23961  clssubg  24019  qustgplem  24031  tsmsres  24054  tsmsxplem1  24063  ucncn  24194  xmettpos  24259  imasdsf1olem  24283  blrnps  24318  blrn  24319  xmeterval  24342  tmslem  24392  tmsxms  24396  imasf1oxms  24399  prdsxms  24440  blval2  24472  metuel2  24475  isngp2  24507  isngp3  24508  tngngp2  24562  isnghm  24633  qtopbaslem  24668  qdensere  24679  cnbl0  24683  cnblcld  24684  cnfldms  24685  blssioo  24705  tgioo  24706  tgqioo  24710  xrtgioo  24717  xrsdsre  24721  xrge0tsms  24745  iimulcnOLD  24857  bndth  24879  lebnumlem3  24884  nmhmcn  25042  cphsqrtcl  25106  lmmbr2  25181  caucfil  25205  causs  25220  lmcau  25235  bcth3  25253  cncms  25277  cnfldcusp  25279  rrxmvallem  25326  ivthicc  25381  ovolfioo  25390  ovolficc  25391  ovolficcss  25392  ovollb2lem  25411  ovoliunlem2  25426  ovolshftlem1  25432  ovolicc2  25445  ismbl  25449  voliunlem2  25474  volsup  25479  ioorf  25496  ioorinv  25499  ioorcl  25500  uniiccdif  25501  uniioovol  25502  uniiccvol  25503  uniioombllem2  25506  uniioombllem4  25509  dyaddisj  25519  dyadmax  25521  dyadmbllem  25522  dyadmbl  25523  opnmbllem  25524  opnmblALT  25526  volsup2  25528  mbfdm  25549  mbfima  25553  mbfid  25558  ismbfd  25562  mbfres2  25568  mbfposr  25575  mbfimaopnlem  25578  mbflimsup  25589  0plef  25595  i1f1lem  25612  itg11  25614  itg1addlem4  25622  i1fpos  25629  itg1le  25636  itg1climres  25637  mbfi1fseqlem5  25642  mbfi1flimlem  25645  xrge0f  25654  itg2ge0  25658  itg2seq  25665  itg2i1fseqle  25677  itg2i1fseq2  25679  itg2addlem  25681  itg2gt0  25683  limciun  25817  dvres  25834  dvres3a  25837  cpnres  25861  dvfre  25877  dvmptres3  25882  dvlip2  25922  dvgt0lem2  25930  deg1fvi  26012  uc1pmon1p  26079  fta1g  26097  ig1peu  26102  ig1pdvds  26107  plyco0  26119  plypf1  26139  dgrlem  26156  dgrub  26161  dgrlb  26163  coemulc  26182  plyreres  26212  plydivlem3  26225  plydivlem4  26226  plydiveu  26228  plyremlem  26234  fta1lem  26237  fta1  26238  vieta1lem2  26241  plyexmo  26243  elaa  26246  elqaalem3  26251  aannenlem1  26258  pserulm  26353  psercnlem2  26356  psercnlem1  26357  psercn  26358  abelth  26373  reeff1o  26379  pilem1  26383  recosf1o  26466  resinf1o  26467  efif1olem3  26475  efif1olem4  26476  efifo  26478  eff1olem  26479  ellogrn  26490  logcn  26578  dvloglem  26579  logf1o2  26581  efopnlem1  26587  efopnlem2  26588  efopn  26589  logtayl  26591  cxpcn3lem  26679  cxpcn3  26680  resqrtcn  26681  asinneg  26818  areambl  26890  emcllem7  26934  lgamgulm2  26968  basellem4  27016  sqff1o  27114  mpodvdsmulf1o  27126  fsumdvdsmul  27127  dvdsmulf1o  27128  fsumdvdsmulOLD  27129  ostthlem1  27560  ostth  27572  noetasuplem4  27670  madeval2  27789  elold  27809  old1  27815  madeoldsuc  27825  tglnfn  28520  f1otrg  28844  axlowdimlem6  28920  axlowdimlem8  28922  axlowdimlem9  28923  axlowdimlem11  28925  axlowdimlem12  28926  axlowdimlem17  28931  elntg2  28958  dfpth2  29702  cyclnumvtx  29773  crctcshlem4  29793  clwlkclwwlklem2  29972  eucrct2eupth  30217  ex-fpar  30434  cnnvm  30654  sspmlem  30704  nvo00  30733  nmlno0lem  30765  phoeqi  30829  ubthlem1  30842  hhip  31149  hhssabloilem  31233  hhssnv  31236  hhsssh  31241  occllem  31275  shsel  31286  chscllem2  31610  df0op2  31724  hoeq  31732  hocofni  31739  hoaddfni  31742  hosubfni  31743  hon0  31765  ho01i  31800  hoeq1  31802  elnlfn  31900  nmlnop0iALT  31967  lnopco0i  31976  imaelshi  32030  nlelchi  32033  rnbra  32079  cnvbraval  32082  kbass5  32092  hmopidmchi  32123  hmopidmpji  32124  foresf1o  32476  fcomptf  32632  ofpreima  32639  resf1o  32705  maprnin  32706  fpwrelmapffslem  32707  hashgt1  32782  indpi1  32833  indpreima  32838  s3clhash  32921  gsumpart  33029  xrge0tsmsd  33034  tocyc01  33079  cyc3evpm  33111  cycpmgcl  33114  cycpmconjslem2  33116  cyc3conja  33118  kerunit  33282  1arithidomlem1  33492  1arithidomlem2  33493  1arithidom  33494  dimval  33605  dimvalfi  33606  ply1degltdimlem  33627  ply1degltdim  33628  elirng  33691  txomap  33839  locfinreflem  33845  hauseqcn  33903  xpinpreima  33911  xpinpreima2  33912  tpr2rico  33917  mndpluscn  33931  raddcn  33934  xrge0pluscn  33945  xrge0tmdALT  33951  rge0scvg  33954  pl1cn  33960  elzrhunit  33982  qqhf  33991  cnrrext  34015  qqhre  34025  1stmbfm  34265  2ndmbfm  34266  mbfmcnt  34273  omssubadd  34305  carsggect  34323  eulerpartlemsv2  34363  eulerpartlems  34365  eulerpartlemv  34369  eulerpartlemb  34373  eulerpartlemf  34375  eulerpartlemt  34376  eulerpartlemmf  34380  eulerpartlemgvv  34381  eulerpartlemgh  34383  eulerpartlemgs2  34385  sseqmw  34396  sseqf  34397  sseqp1  34400  fiblem  34403  fibp1  34406  plymul02  34551  signsvtn0  34575  signstres  34580  signshlen  34595  reprinrn  34623  circlemethhgt  34648  txsconnlem  35276  iccllysconn  35286  rellysconn  35287  cvmseu  35312  cvmliftmolem2  35318  cvmliftlem6  35326  cvmliftlem7  35327  cvmliftlem8  35328  cvmliftlem9  35329  cvmliftlem11  35331  cvmliftlem15  35334  cvmlift2lem7  35345  cvmlift2lem10  35348  cvmlift3lem8  35362  cvmlift3lem9  35363  mvrsfpw  35542  mrsubff1  35550  msrid  35581  msrfo  35582  elmsta  35584  mtyf  35588  msubff1  35592  vhmcls  35602  mclsax  35605  elmthm  35612  mthmblem  35616  mclsppslem  35619  iprodefisumlem  35776  fullfunfnv  35980  fullfunfv  35981  tailfb  36411  filnetlem4  36415  taupilem3  37353  icoreresf  37386  icoreelrnab  37388  relowlssretop  37397  relowlpssretop  37398  unccur  37643  matunitlindflem1  37656  matunitlindflem2  37657  ptrecube  37660  poimirlem28  37688  poimirlem32  37692  heicant  37695  opnmbllem0  37696  mblfinlem1  37697  mblfinlem2  37698  volsupnfl  37705  cnambfre  37708  dvtan  37710  itg2addnclem  37711  itg2addnclem2  37712  ftc1anclem3  37735  ftc1anclem5  37737  ftc1anclem7  37739  ftc1anclem8  37740  ftc1anc  37741  areacirc  37753  indexdom  37774  sdclem2  37782  sstotbnd2  37814  sstotbnd  37815  isbndx  37822  isbnd3b  37825  prdsbnd  37833  prdstotbnd  37834  ismtyhmeolem  37844  heibor1lem  37849  heiborlem1  37851  heibor  37861  rrnequiv  37875  keridl  38072  ellkr  39128  lkr0f  39133  cdleme50rnlem  40583  aks6d1c2lem4  42160  aks6d1c5  42172  sticksstones11  42189  sticksstones19  42198  sticksstones22  42201  aks6d1c6lem4  42206  aks6d1c6isolem2  42208  fsuppind  42623  elrfirn  42728  ismrcd2  42732  isnacs2  42739  nacsfix  42745  mapfzcons1  42750  mzpcompact2lem  42784  eq0rabdioph  42809  eldioph4b  42844  diophren  42846  pw2f1ocnv  43070  pw2f1o2val2  43073  lmhmfgsplit  43119  pwssplit4  43122  hbt  43163  mpaaeu  43183  mendring  43221  proot1mul  43227  proot1hash  43228  proot1ex  43229  deg1mhm  43233  fgraphopab  43236  hausgraph  43238  nvocnvb  43455  ofsubid  44357  expgrowthi  44366  expgrowth  44368  binomcxplemdvbinom  44386  binomcxplemcvg  44387  binomcxplemnotnn0  44389  relpfrlem  44986  rfcnpre1  45056  rfcnpre2  45068  cncmpmax  45069  rfcnpre3  45070  rfcnpre4  45071  elixpconstg  45126  ffi  45210  islptre  45659  resincncf  45913  dvcosre  45950  dvresntr  45956  volioof  46025  stoweidlem48  46086  fourierdlem12  46157  fourierdlem15  46160  fourierdlem41  46186  fourierdlem42  46187  fourierdlem46  46190  fourierdlem48  46192  fourierdlem49  46193  fourierdlem54  46198  fourierdlem56  46200  fourierdlem62  46206  fourierdlem64  46208  fourierdlem65  46209  fourierdlem73  46217  fourierdlem74  46218  fourierdlem75  46219  fourierdlem102  46246  fourierdlem103  46247  fourierdlem104  46248  fourierdlem114  46258  sge0split  46447  elhoi  46580  mbfresmf  46777  cjnpoly  46920  cfsetsnfsetf1  47090  cfsetsnfsetfo  47091  focofob  47111  f1ocof1ob  47112  fafvelcdm  47201  ffnafv  47202  fafv2elcdm  47265  fafv2elrnb  47266  imarnf1pr  47313  2ffzoeq  47358  fundcmpsurbijinjpreimafv  47438  fundcmpsurinjimaid  47442  fargshiftfv  47470  fargshiftf  47471  fargshiftf1  47472  fargshiftfo  47473  cycl3grtri  47978  fdmdifeqresdif  48373  fdivmpt  48572  fdivmptf  48573  refdivmptf  48574  1arymaptf1  48674  2arymaptf1  48685  ackfnnn0  48717  homf0  49041  aacllem  49833