Theorem ffn 6668

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

Syntax hints:   → wi 4   ⊆ wss 3889  ran crn 5632   Fn wfn 6493  ⟶wf 6494

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 6502

This theorem is referenced by:  ffnd  6669  ffun  6671  frel  6673  fdm  6677  ffrn  6681  fresin  6709  fresaun  6711  fresaunres2  6712  fcoi1  6714  feu  6716  f0bi  6723  dffo2  6756  fimadmfo  6761  fdmeu  6896  feqmptdf  6910  fimarab  6914  fvco3  6939  ffvelcdm  7033  dff2  7051  dffo3  7054  dffo4  7055  dffo5  7056  dffo3f  7058  f1ompt  7063  ffnfv  7071  fcdmssb  7074  fcompt  7086  fsn2  7089  fprb  7149  fconst2g  7158  fpr2g  7166  fex  7181  dff13  7209  nvocnv  7236  soisores  7282  fdmexb  7858  resf1extb  7885  fo1stres  7968  fo2ndres  7969  1stcof  7972  2ndcof  7973  curry1f  8056  curry2f  8058  fparlem1  8062  fparlem2  8063  fo2ndf  8071  soseq  8109  tposf2  8200  smo11  8304  fsetexb  8811  mapsnd  8834  pw2f1olem  9019  mapen  9079  mapunen  9084  fissuni  9267  fipreima  9268  indexfi  9270  mapfien  9321  oismo  9455  cantnflt  9593  cantnfp1lem3  9601  cantnflem4  9613  tcrank  9808  updjudhcoinlf  9856  updjudhcoinrg  9857  updjud  9858  infpwfien  9984  cardinfima  10019  dfacacn  10064  cfflb  10181  cofsmo  10191  cfcoflem  10194  coftr  10195  fin23lem40  10273  axdc3lem2  10373  ac6num  10401  ac6c4  10403  ac6s2  10408  ttukeylem6  10436  iunfo  10461  pwcfsdom  10506  fpwwe2lem5  10558  fpwwe2lem7  10560  pwfseqlem3  10583  inar1  10698  tskcard  10704  tskuni  10706  tskurn  10712  gruima  10725  nqerrel  10855  recmulnq  10887  dmrecnq  10891  axpre-sup  11092  ofsubeq0  12156  indpi1  12173  dfz2  12543  uzn0  12805  rpnnen1lem3  12929  rpnnen1lem5  12931  unirnioo  13402  dfioo2  13403  ioorebas  13404  fseq1p1m1  13552  2ffzeq  13603  fvinim0ffz  13744  injresinjlem  13745  fsequb2  13938  fseqsupcl  13939  fseqsupubi  13940  ser0f  14017  hashgval  14295  hashinf  14297  hashresfn  14302  ffz0hash  14409  fnfzo0hash  14412  wrdred1hash  14523  revlen  14724  revrev  14729  repswlen  14738  repsdf2  14740  cshword  14753  0csh0  14755  lenco  14794  s1co  14795  cshco  14798  swrdco  14799  s7f1o  14928  ofccat  14931  shftf  15041  uzin2  15307  rexanuz  15308  limsuple  15440  limsupval2  15442  rlimres  15520  lo1res  15521  rlimresb  15527  isercolllem2  15628  isercolllem3  15629  isercoll  15630  supcvg  15821  prodf1f  15857  eff2  16066  reeff1  16087  tanval  16095  ruclem4  16201  ruclem12  16208  prmreclem6  16892  1arithlem4  16897  1arith  16898  vdwmc  16949  vdwlem1  16952  vdwlem8  16959  vdwlem13  16964  ramval  16979  0ram  16991  0ram2  16992  0ramcl  16994  ramcl  17000  fsets  17139  firest  17395  0ssc  17804  0subcat  17805  isfull2  17880  arwhoma  18012  gsumval2a  18653  isgrpinv  18969  kerf1ghm  19222  f1omvdconj  19421  pmtrmvd  19431  pmtrfinv  19436  pmtrdifellem4  19454  efgsfo  19714  efgredlem  19722  efgcpbllemb  19730  frgpup3lem  19752  0frgp  19754  gexex  19828  torsubg  19829  gsumval3  19882  gsumzres  19884  gsummptmhm  19915  gsumzoppg  19919  dprdf1o  20009  dprd2db  20020  zrinitorngc  20619  zrtermorngc  20620  zrtermoringc  20652  srngf1o  20825  lmhmima  21042  lmhmpreima  21043  lmhmrnlss  21045  lspextmo  21051  pwssplit1  21054  cnfldadd  21358  cnfldmul  21360  cnfldplusf  21379  cnfldsub  21380  chrrhm  21511  znunit  21543  psgnevpmb  21567  psgndiflemB  21580  mpofrlmd  21757  frlmipval  21759  frlmphl  21761  frlmlbs  21777  frlmup4  21781  ellspd  21782  lindfmm  21807  lsslindf  21810  psrbaglefi  21906  psrlidm  21940  mplmonmul  22014  evlseu  22061  mpfconst  22087  mpfproj  22088  mpfsubrg  22089  coe1sclmulfv  22248  pf1const  22311  pf1id  22312  pf1subrg  22313  mpfpf1  22316  pf1mpf  22317  mamuass  22367  mamudi  22368  mamudir  22369  mamuvs1  22370  mamuvs2  22371  1mavmul  22513  mavmulass  22514  mdetunilem7  22583  madutpos  22607  lecldbas  23184  lmbr2  23224  cncnpi  23243  cncnp  23245  cnpdis  23258  lmff  23266  pnrmopn  23308  dnsconst  23343  cmpsub  23365  tgcmp  23366  hauscmplem  23371  2ndcctbss  23420  2ndcomap  23423  2ndcsep  23424  1stccnp  23427  kgenidm  23512  iskgen2  23513  1stckgen  23519  kgen2cn  23524  ptpjpre1  23536  pttop  23547  ptuni  23559  ptval2  23566  tx1cn  23574  tx2cn  23575  ptpjcn  23576  ptpjopn  23577  ptclsg  23580  ptcnplem  23586  upxp  23588  txcnmpt  23589  uptx  23590  txcmplem2  23607  txkgen  23617  xkoptsub  23619  xkopt  23620  xkococnlem  23624  xkococn  23625  ptcmpfi  23778  zfbas  23861  uzrest  23862  rnelfmlem  23917  rnelfm  23918  fmfnfmlem2  23920  fmfnfm  23923  lmflf  23970  alexsubALT  24016  clssubg  24074  qustgplem  24086  tsmsres  24109  tsmsxplem1  24118  ucncn  24249  xmettpos  24314  imasdsf1olem  24338  blrnps  24373  blrn  24374  xmeterval  24397  tmslem  24447  tmsxms  24451  imasf1oxms  24454  prdsxms  24495  blval2  24527  metuel2  24530  isngp2  24562  isngp3  24563  tngngp2  24617  isnghm  24688  qtopbaslem  24723  qdensere  24734  cnbl0  24738  cnblcld  24739  cnfldms  24740  blssioo  24760  tgioo  24761  tgqioo  24765  xrtgioo  24772  xrsdsre  24776  xrge0tsms  24800  bndth  24925  lebnumlem3  24930  nmhmcn  25087  cphsqrtcl  25151  lmmbr2  25226  caucfil  25250  causs  25265  lmcau  25280  bcth3  25298  cncms  25322  cnfldcusp  25324  rrxmvallem  25371  ivthicc  25425  ovolfioo  25434  ovolficc  25435  ovolficcss  25436  ovollb2lem  25455  ovoliunlem2  25470  ovolshftlem1  25476  ovolicc2  25489  ismbl  25493  voliunlem2  25518  volsup  25523  ioorf  25540  ioorinv  25543  ioorcl  25544  uniiccdif  25545  uniioovol  25546  uniiccvol  25547  uniioombllem2  25550  uniioombllem4  25553  dyaddisj  25563  dyadmax  25565  dyadmbllem  25566  dyadmbl  25567  opnmbllem  25568  opnmblALT  25570  volsup2  25572  mbfdm  25593  mbfima  25597  mbfid  25602  ismbfd  25606  mbfres2  25612  mbfposr  25619  mbfimaopnlem  25622  mbflimsup  25633  0plef  25639  i1f1lem  25656  itg11  25658  itg1addlem4  25666  i1fpos  25673  itg1le  25680  itg1climres  25681  mbfi1fseqlem5  25686  mbfi1flimlem  25689  xrge0f  25698  itg2ge0  25702  itg2seq  25709  itg2i1fseqle  25721  itg2i1fseq2  25723  itg2addlem  25725  itg2gt0  25727  limciun  25861  dvres  25878  dvres3a  25881  cpnres  25904  dvfre  25918  dvmptres3  25923  dvlip2  25962  dvgt0lem2  25970  deg1fvi  26050  uc1pmon1p  26117  fta1g  26135  ig1peu  26140  ig1pdvds  26145  plyco0  26157  plypf1  26177  dgrlem  26194  dgrub  26199  dgrlb  26201  coemulc  26220  plyreres  26249  plydivlem3  26261  plydivlem4  26262  plydiveu  26264  plyremlem  26270  fta1lem  26273  fta1  26274  vieta1lem2  26277  plyexmo  26279  elaa  26282  elqaalem3  26287  aannenlem1  26294  pserulm  26387  psercnlem2  26389  psercnlem1  26390  psercn  26391  abelth  26406  reeff1o  26412  pilem1  26416  recosf1o  26499  resinf1o  26500  efif1olem3  26508  efif1olem4  26509  efifo  26511  eff1olem  26512  ellogrn  26523  logcn  26611  dvloglem  26612  logf1o2  26614  efopnlem1  26620  efopnlem2  26621  efopn  26622  logtayl  26624  cxpcn3lem  26711  cxpcn3  26712  resqrtcn  26713  asinneg  26850  areambl  26922  emcllem7  26965  lgamgulm2  26999  basellem4  27047  sqff1o  27145  mpodvdsmulf1o  27157  fsumdvdsmul  27158  dvdsmulf1o  27159  ostthlem1  27590  ostth  27602  noetasuplem4  27700  madeval2  27825  elold  27851  old1  27857  madeoldsuc  27877  tglnfn  28615  f1otrg  28939  axlowdimlem6  29016  axlowdimlem8  29018  axlowdimlem9  29019  axlowdimlem11  29021  axlowdimlem12  29022  axlowdimlem17  29027  elntg2  29054  dfpth2  29797  cyclnumvtx  29868  crctcshlem4  29888  clwlkclwwlklem2  30070  eucrct2eupth  30315  ex-fpar  30532  cnnvm  30753  sspmlem  30803  nvo00  30832  nmlno0lem  30864  phoeqi  30928  ubthlem1  30941  hhip  31248  hhssabloilem  31332  hhssnv  31335  hhsssh  31340  occllem  31374  shsel  31385  chscllem2  31709  df0op2  31823  hoeq  31831  hocofni  31838  hoaddfni  31841  hosubfni  31842  hon0  31864  ho01i  31899  hoeq1  31901  elnlfn  31999  nmlnop0iALT  32066  lnopco0i  32075  imaelshi  32129  nlelchi  32132  rnbra  32178  cnvbraval  32181  kbass5  32191  hmopidmchi  32222  hmopidmpji  32223  foresf1o  32574  fcomptf  32731  ofpreima  32738  resf1o  32803  maprnin  32804  fpwrelmapffslem  32805  hashgt1  32881  indpreima  32925  s3clhash  33008  gsumpart  33124  xrge0tsmsd  33134  tocyc01  33179  cyc3evpm  33211  cycpmgcl  33214  cycpmconjslem2  33216  cyc3conja  33218  kerunit  33385  1arithidomlem1  33595  1arithidomlem2  33596  1arithidom  33597  psrmonmul  33694  dimval  33745  dimvalfi  33746  ply1degltdimlem  33766  ply1degltdim  33767  elirng  33830  txomap  33978  locfinreflem  33984  hauseqcn  34042  xpinpreima  34050  xpinpreima2  34051  tpr2rico  34056  mndpluscn  34070  raddcn  34073  xrge0pluscn  34084  xrge0tmdALT  34090  rge0scvg  34093  pl1cn  34099  elzrhunit  34121  qqhf  34130  cnrrext  34154  qqhre  34164  1stmbfm  34404  2ndmbfm  34405  mbfmcnt  34412  omssubadd  34444  carsggect  34462  eulerpartlemsv2  34502  eulerpartlems  34504  eulerpartlemv  34508  eulerpartlemb  34512  eulerpartlemf  34514  eulerpartlemt  34515  eulerpartlemmf  34519  eulerpartlemgvv  34520  eulerpartlemgh  34522  eulerpartlemgs2  34524  sseqmw  34535  sseqf  34536  sseqp1  34539  fiblem  34542  fibp1  34545  plymul02  34690  signsvtn0  34714  signstres  34719  signshlen  34734  reprinrn  34762  circlemethhgt  34787  txsconnlem  35422  iccllysconn  35432  rellysconn  35433  cvmseu  35458  cvmliftmolem2  35464  cvmliftlem6  35472  cvmliftlem7  35473  cvmliftlem8  35474  cvmliftlem9  35475  cvmliftlem11  35477  cvmliftlem15  35480  cvmlift2lem7  35491  cvmlift2lem10  35494  cvmlift3lem8  35508  cvmlift3lem9  35509  mvrsfpw  35688  mrsubff1  35696  msrid  35727  msrfo  35728  elmsta  35730  mtyf  35734  msubff1  35738  vhmcls  35748  mclsax  35751  elmthm  35758  mthmblem  35762  mclsppslem  35765  iprodefisumlem  35922  fullfunfnv  36128  fullfunfv  36129  tailfb  36559  filnetlem4  36563  regsfromunir1  36722  taupilem3  37633  icoreresf  37668  icoreelrnab  37670  relowlssretop  37679  relowlpssretop  37680  unccur  37924  matunitlindflem1  37937  matunitlindflem2  37938  ptrecube  37941  poimirlem28  37969  poimirlem32  37973  heicant  37976  opnmbllem0  37977  mblfinlem1  37978  mblfinlem2  37979  volsupnfl  37986  cnambfre  37989  dvtan  37991  itg2addnclem  37992  itg2addnclem2  37993  ftc1anclem3  38016  ftc1anclem5  38018  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  areacirc  38034  indexdom  38055  sdclem2  38063  sstotbnd2  38095  sstotbnd  38096  isbndx  38103  isbnd3b  38106  prdsbnd  38114  prdstotbnd  38115  ismtyhmeolem  38125  heibor1lem  38130  heiborlem1  38132  heibor  38142  rrnequiv  38156  keridl  38353  ellkr  39535  lkr0f  39540  cdleme50rnlem  40990  aks6d1c2lem4  42566  aks6d1c5  42578  sticksstones11  42595  sticksstones19  42604  sticksstones22  42607  aks6d1c6lem4  42612  aks6d1c6isolem2  42614  fsuppind  43023  elrfirn  43127  ismrcd2  43131  isnacs2  43138  nacsfix  43144  mapfzcons1  43149  mzpcompact2lem  43183  eq0rabdioph  43208  eldioph4b  43239  diophren  43241  pw2f1ocnv  43465  pw2f1o2val2  43468  lmhmfgsplit  43514  pwssplit4  43517  hbt  43558  mpaaeu  43578  mendring  43616  proot1mul  43622  proot1hash  43623  proot1ex  43624  deg1mhm  43628  fgraphopab  43631  hausgraph  43633  nvocnvb  43849  ofsubid  44751  expgrowthi  44760  expgrowth  44762  binomcxplemdvbinom  44780  binomcxplemcvg  44781  binomcxplemnotnn0  44783  relpfrlem  45380  rfcnpre1  45450  rfcnpre2  45462  cncmpmax  45463  rfcnpre3  45464  rfcnpre4  45465  elixpconstg  45519  ffi  45603  islptre  46049  resincncf  46303  dvcosre  46340  dvresntr  46346  volioof  46415  stoweidlem48  46476  fourierdlem12  46547  fourierdlem15  46550  fourierdlem41  46576  fourierdlem42  46577  fourierdlem46  46580  fourierdlem48  46582  fourierdlem49  46583  fourierdlem54  46588  fourierdlem56  46590  fourierdlem62  46596  fourierdlem64  46598  fourierdlem65  46599  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem102  46636  fourierdlem103  46637  fourierdlem104  46638  fourierdlem114  46648  sge0split  46837  elhoi  46970  mbfresmf  47167  cjnpoly  47337  cfsetsnfsetf1  47507  cfsetsnfsetfo  47508  focofob  47528  f1ocof1ob  47529  fafvelcdm  47618  ffnafv  47619  fafv2elcdm  47682  fafv2elrnb  47683  imarnf1pr  47730  2ffzoeq  47776  fundcmpsurbijinjpreimafv  47867  fundcmpsurinjimaid  47871  fargshiftfv  47899  fargshiftf  47900  fargshiftf1  47901  fargshiftfo  47902  cycl3grtri  48423  fdmdifeqresdif  48818  fdivmpt  49016  fdivmptf  49017  refdivmptf  49018  1arymaptf1  49118  2arymaptf1  49129  ackfnnn0  49161  homf0  49484  aacllem  50276