Theorem ffnd 6657

Description: A mapping is a function with domain, deduction form. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Hypothesis

Ref	Expression
ffnd.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)

Assertion

Ref	Expression
ffnd	⊢ (𝜑 → 𝐹 Fn 𝐴)

Proof of Theorem ffnd

Step	Hyp	Ref	Expression
1		ffnd.1	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		ffn 6656	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 6481  ⟶wf 6482

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 6490

This theorem is referenced by:  fnconstg  6716  f1fn  6725  fofn  6742  f1ofn  6769  feqmptd  6896  fssrescdmd  7065  fprb  7134  cocan1  7231  oprres  7520  off  7634  coof  7640  ofco  7641  caofref  7647  caofid0l  7649  caofid0r  7650  caofid1  7651  caofid2  7652  caofrss  7655  caoftrn  7657  fo2ndf  8057  fnwelem  8067  fnse  8069  suppsnop  8114  suppss  8130  suppssr  8131  suppssrg  8132  suppssof1  8135  suppofssd  8139  suppofss1d  8140  suppofss2d  8141  suppcoss  8143  smocdmdom  8294  elmapfn  8795  ralxpmap  8826  omxpenlem  8998  mapen  9061  f1finf1o  9164  unirnffid  9238  fdmfifsupp  9266  mapfien  9299  intrnfi  9307  marypha2  9330  ordtypelem7  9417  wemapsolem  9443  wemapso  9444  wemapso2lem  9445  unxpwdom2  9481  ixpiunwdom  9483  cantnfle  9568  cantnfp1lem2  9576  cantnfp1lem3  9577  cantnfp1  9578  oemapvali  9581  cantnflem1a  9582  cantnflem1c  9584  cantnflem3  9588  cantnf  9590  cnfcomlem  9596  cnfcom3  9601  updjudhcoinlf  9832  updjudhcoinrg  9833  fseqenlem1  9922  numacn  9947  infpwfien  9960  isf32lem2  10252  isf34lem7  10277  isf34lem6  10278  unirnfdomd  10465  ofsubeq0  12129  ofnegsub  12130  ofsubge0  12131  seqf1olem2  13951  resunimafz0  14354  wrdfn  14437  swrdvalfn  14561  pfxfn  14591  pfxid  14594  cats1un  14630  cshwfn  14710  ccatco  14744  limsupgle  15386  o1of2  15522  o1rlimmul  15528  isercolllem2  15575  isercoll  15577  isercoll2  15578  climsup  15579  fsumss  15634  ruclem11  16151  vdwlem2  16896  vdwlem6  16900  vdwlem9  16903  vdwlem12  16906  0ram  16934  ramub1lem1  16940  pwsle  17398  pwsleval  17399  pwsvscaval  17401  mrcuni  17529  mrcun  17530  invf1o  17678  funcres2c  17812  setcmon  17996  setcepi  17997  uncfcurf  18147  yoniso  18193  isacs4lem  18452  acsmapd  18462  chnso  18532  gsumval2  18596  mgmhmf1o  18610  resmgmhm2b  18623  mgmhmima  18625  mgmhmeql  18626  prdsplusgsgrpcl  18642  prdssgrpd  18643  prdsplusgcl  18678  prdsidlem  18679  prdsmndd  18680  mhmf1o  18706  resmhm2b  18732  mhmimalem  18734  mhmima  18735  mhmeql  18736  prdspjmhm  18739  pwsco1mhm  18742  pwsco2mhm  18743  gsumwmhm  18755  frmdss2  18773  grpinvf1o  18924  prdsinvlem  18964  cycsubgcl  19120  ghmrn  19143  ghmpreima  19152  ghmeql  19153  ghmnsgima  19154  ghmnsgpreima  19155  ghmeqker  19157  ghmf1o  19162  ghmqusnsglem1  19194  ghmqusnsg  19196  ghmquskerlem1  19197  ghmquskerco  19198  ghmquskerlem3  19200  ghmqusker  19201  gass  19215  cntzmhm  19255  symgextres  19339  gsmsymgrfixlem1  19341  fvcosymgeq  19343  f1omvdconj  19360  pmtrfinv  19375  symgtrinv  19386  pmtr3ncomlem1  19387  sygbasnfpfi  19426  efginvrel2  19641  efgredleme  19657  ghmplusg  19760  prdscmnd  19775  gsumval3a  19817  gsumval3eu  19818  gsumzaddlem  19835  gsumzsplit  19841  gsumpt  19876  prdsgsum  19895  dprdfcntz  19931  dprdfadd  19936  dprdfeq0  19938  dprdf11  19939  dprdlub  19942  dprdspan  19943  dprd2dlem1  19957  dmdprdpr  19965  dprdpr  19966  dpjlem  19967  ablfac1eu  19989  gsumle  20059  prdsmulrngcl  20095  prdsrngd  20096  prdsringd  20241  prdscrngd  20242  prds1  20243  pwspjmhmmgpd  20248  rnghmf1o  20372  rhmf1o  20410  rhmimasubrnglem  20482  rnrhmsubrg  20522  rrgsupp  20618  imadrhmcl  20714  isabvd  20729  lmodfopnelem1  20833  lcomfsupp  20837  prdsvscacl  20903  prdslmodd  20904  lmhmco  20979  lmhmplusg  20980  lmhmvsca  20981  lmhmf1o  20982  lmhmeql  20991  lspextmo  20992  rhmpreimaidl  21216  pjfo  21654  dsmmbas2  21676  dsmm0cl  21679  dsmmacl  21680  dsmmsubg  21682  dsmmlss  21683  frlmvplusgvalc  21706  frlmvscaval  21707  frlmplusgvalb  21708  frlmvscavalb  21709  frlmsslss2  21714  frlmphllem  21719  frlmphl  21720  frlmssuvc2  21734  frlmsslsp  21735  frlmup1  21737  frlmup2  21738  frlmup3  21739  frlmup4  21740  islindf4  21777  psrbagfsupp  21858  psrbaglesupp  21861  psrbaglecl  21862  psrbagaddcl  21863  psrbagcon  21864  psrbaglefi  21865  psrbagleadd1  21867  psrbagconf1o  21868  gsumbagdiaglem  21869  psrass1lem  21871  psrvscaval  21889  psrlidm  21900  psrridm  21901  psrass1  21902  psrdi  21903  psrdir  21904  psrascl  21917  mvrf2  21931  mplsubglem  21937  mplvscaval  21954  subrgmvrf  21970  mplbas2  21978  mplind  22006  psrbagev1  22013  psrbagev2  22014  evlslem3  22016  evlslem1  22018  evlsvar  22026  mpfind  22043  ismhp3  22058  mhpmulcl  22065  psdmplcl  22078  psdadd  22079  psdvsca  22080  psdmul  22082  psdmvr  22085  psrplusgpropd  22149  coe1add  22179  coe1addfv  22180  evl1addd  22257  evl1subd  22258  evl1muld  22259  pf1mpf  22268  pf1ind  22271  evls1fpws  22285  ressply1evl  22286  rhmply1vsca  22304  mamudir  22320  mamulid  22357  mamurid  22358  mdetrlin  22518  mdetrsca  22519  mdetralt  22524  mdetunilem7  22534  mdetunilem9  22536  madurid  22560  cnrest2  23202  lmss  23214  lmcnp  23220  cnt0  23262  cnt1  23266  cnhaus  23270  rncmp  23312  conncn  23342  2ndcomap  23374  1stccnp  23378  comppfsc  23448  1stckgenlem  23469  ptbasfi  23497  ptopn  23499  ptclsg  23531  ptcnp  23538  upxp  23539  txtube  23556  txcmplem1  23557  hauseqlcld  23562  xkohaus  23569  xkoptsub  23570  cnmpt11  23579  cnmpt21  23587  cnmpt22f  23591  cnmptcom  23594  qtopss  23631  qtopeu  23632  qtopomap  23634  qtopcmap  23635  kqffn  23641  hmeof1o2  23679  xkocnv  23730  rnelfm  23869  ptcmplem1  23968  cnextfres1  23984  ghmcnp  24031  tgphaus  24033  prdstmdd  24040  prdstgpd  24041  fmucnd  24207  psmetxrge0  24229  isxmet2d  24243  prdsmet  24286  blelrnps  24332  blelrn  24333  xmetresbl  24353  comet  24429  stdbdxmet  24431  met2ndci  24438  prdsxmslem2  24445  isngp3  24514  nmotri  24655  metdsre  24770  bndth  24885  evth  24886  fmcfil  25200  bcthlem4  25255  rrxcph  25320  rrxds  25321  rrxmet  25336  evthicc2  25389  ovolfsf  25400  ovolmge0  25406  ovollb2lem  25417  ovolunlem1a  25425  ovoliunlem1  25431  ovoliun  25434  ovoliun2  25435  ovolscalem1  25442  ovolicc1  25445  ovolicc2lem4  25449  ovolicc2  25451  voliunlem1  25479  voliunlem3  25481  volsup  25485  ioombl1lem2  25488  ioombl1lem4  25490  uniiccdif  25507  uniioombllem2  25512  uniioombllem3  25514  uniioombllem6  25517  volsup2  25534  vitalilem4  25540  mbfeqalem1  25570  mbfmulc2lem  25576  mbfmax  25578  mbfaddlem  25589  mbfadd  25590  mbfsub  25591  mbfsup  25593  mbfinf  25594  itg1ge0  25615  itg1addlem1  25621  i1faddlem  25622  i1fmullem  25623  i1fadd  25624  i1fmul  25625  itg1addlem4  25628  i1fmulclem  25631  i1fmulc  25632  itg1mulc  25633  i1fres  25634  itg10a  25639  itg1ge0a  25640  itg1lea  25641  mbfi1fseqlem3  25646  mbfi1fseqlem4  25647  mbfi1flimlem  25651  mbfmullem2  25653  mbfmul  25655  itg20  25666  itg2lea  25673  itg2splitlem  25677  itg2split  25678  itg2monolem1  25679  itg2monolem2  25680  itg2monolem3  25681  itg2mono  25682  itg2i1fseqle  25683  itg2i1fseq  25684  itg2addlem  25687  itg2gt0  25689  itg2cnlem1  25690  itg2cnlem2  25691  itg2cn  25692  itgitg1  25738  bddmulibl  25768  bddibl  25769  dvidlem  25844  dvaddbr  25868  dvmulbr  25869  dvmulbrOLD  25870  dvaddf  25873  dvcmulf  25876  dvrec  25887  dvcnvlem  25908  rolle  25922  dveq0  25933  dv11cn  25934  dvivthlem2  25942  dvivth  25943  dvne0  25944  lhop1lem  25946  lhop1  25947  lhop2  25948  lhop  25949  ftc1cn  25978  tdeglem1  25991  tdeglem3  25992  tdeglem4  25993  mdegleb  25997  mdegldg  25999  mdegaddle  26007  ply1remlem  26098  ply1rem  26099  fta1glem1  26101  fta1glem2  26102  fta1blem  26104  idomrootle  26106  plyeq0lem  26143  plyeq0  26144  plyaddlem1  26146  coeeulem  26157  coeaddlem  26182  coemulc  26188  dgradd2  26202  dgrcolem2  26208  ofmulrt  26217  plyrem  26241  vieta1lem1  26246  vieta1  26248  plyexmo  26249  elqaalem3  26257  aannenlem1  26264  aalioulem2  26269  ulmuni  26329  ulmdvlem1  26337  ulmdv  26340  mbfulm  26343  iblulm  26344  itgulm  26345  rlimcnp2  26904  jensen  26927  amgm  26929  basellem3  27021  basellem7  27025  basellem9  27027  dchrelbas2  27176  dchrmulcl  27188  dchrfi  27194  dchreq  27197  dchrresb  27198  dchrinv  27200  dchr1re  27202  sumdchr2  27209  dchr2sum  27212  lgsqrlem2  27286  lgsqrlem3  27287  rpvmasum2  27451  dchrisum0re  27452  mirf1o  28648  lmif1o  28774  eqeefv  28883  axlowdimlem14  28935  vtxdgfisf  29457  2pthon3v  29923  nvinvfval  30622  sspg  30710  ssps  30712  sspmlem  30714  sspn  30718  lnon0  30780  ubthlem1  30852  pjfn  31691  kbpj  31938  kbass2  32099  elpjrn  32172  ofrn2  32624  off2  32625  ofresid  32626  xppreima2  32635  ofpreima2  32650  suppovss  32666  resf1o  32717  prodindf  32851  indpreima  32853  swrdrn3  32943  pwrssmgc  32988  mgcf1o  32991  gsumfs2d  33042  gsumhashmul  33048  symgcom2  33060  pmtrcnel  33065  pmtrcnel2  33066  pmtrcnelor  33067  cycpmfvlem  33088  cycpmfv3  33091  cycpmcl  33092  cycpmco2rn  33101  cycpmco2  33109  cycpm3cl2  33112  cyc3co2  33116  cyc3evpm  33126  elrgspnlem1  33216  elrgspnlem2  33217  elrgspnlem4  33219  elrgspnsubrunlem1  33221  elrgspnsubrunlem2  33222  gsumind  33317  islinds5  33339  ellspds  33340  elrspunidl  33400  elrspunsn  33401  rhmimaidl  33404  rhmpreimaprmidl  33423  rprmdvdsprod  33506  1arithidomlem2  33508  evls1fn  33530  ply1dg1rt  33550  ply1mulrtss  33552  ply1degltel  33562  ply1degleel  33563  ply1degltlss  33564  ply1gsumz  33566  ig1pmindeg  33569  r1pquslmic  33578  extvfvcl  33587  mplmulmvr  33590  mplvrpmmhm  33594  mplvrpmrhm  33595  esplyfval2  33605  esplyfv1  33609  esplyfv  33610  esplyfval3  33612  esplyind  33613  exsslsb  33630  ply1degltdimlem  33656  ply1degltdim  33657  dimkerim  33661  fedgmullem2  33664  fedgmul  33665  lvecendof1f1o  33667  fldextrspunlsplem  33707  fldextrspunlsp  33708  irngss  33721  irngnzply1  33725  extdgfialglem2  33727  irngnminplynz  33746  2sqr3minply  33814  cos9thpiminply  33822  cmpcref  33884  rhmpreimacnlem  33918  fsumcvg4  33984  pl1cn  33989  qqhval2lem  34015  esumcvg  34120  ofcf  34137  ofcof  34141  measfn  34238  meascnbl  34253  sibfof  34374  sitgaddlemb  34382  subiwrdlen  34420  rrvfn  34479  plymul02  34580  signsplypnf  34584  signsply0  34585  reprsuc  34649  reprdifc  34661  breprexplema  34664  circlemethhgt  34677  hgt750lemb  34690  f1resrcmplf1dlem  35119  pthhashvtx  35193  cvmopnlem  35343  cvmliftmolem1  35346  cvmliftlem10  35359  cvmlift2lem9a  35368  cvmlift2lem6  35373  cvmlift2lem12  35379  cvmliftphtlem  35382  cvmlift3lem9  35392  mrsubrn  35578  elmrsubrn  35585  elmsubrn  35593  msubrn  35594  mclsind  35635  mclsppslem  35648  mclspps  35649  iprodefisumlem  35805  weiunfrlem  36529  matunitlindflem1  37676  poimirlem1  37681  poimirlem2  37682  poimirlem3  37683  poimirlem16  37696  poimirlem17  37697  poimirlem19  37699  poimirlem20  37700  poimirlem22  37702  poimirlem23  37703  poimirlem29  37709  poimirlem30  37710  poimirlem31  37711  poimir  37713  mblfinlem2  37718  itg2addnclem3  37733  itg2addnc  37734  itg2gt0cn  37735  ftc1cnnc  37752  ftc1anclem5  37757  ftc1anclem7  37759  ftc1anc  37761  sdclem2  37802  istotbnd3  37831  sstotbnd2  37834  isbnd3  37844  heibor1lem  37869  rrnmet  37889  grpokerinj  37953  isdrngo2  38018  lfl1  39189  lfladdcl  39190  lflvscl  39196  lkr0f  39213  lkrsc  39216  eqlkr2  39219  eqlkr3  39220  ldualvaddval  39250  ldualvsval  39257  tendoeq1  40883  zndvdchrrhm  42085  hashscontpow  42235  aks6d1c3  42236  aks6d1c2lem4  42240  aks6d1c2  42243  sticksstones1  42259  sticksstones2  42260  sticksstones3  42261  sticksstones12a  42270  sticksstones12  42271  aks6d1c6lem2  42284  aks6d1c6lem3  42285  aks6d1c6isolem1  42287  aks6d1c6isolem3  42289  aks6d1c6lem5  42290  aks6d1c7lem1  42293  unitscyglem1  42308  dvun  42477  frlmvscadiccat  42624  fiabv  42654  frlmsnic  42658  pwsgprod  42662  mplmapghm  42674  evlsvvval  42681  evlsaddval  42686  evlsmulval  42687  evladdval  42693  evlmulval  42694  selvvvval  42703  evlselvlem  42704  evlselv  42705  fsuppssind  42711  mhphf  42715  ismrcd1  42815  ismrcd2  42816  istopclsd  42817  isnacs3  42827  mzpaddmpt  42858  mzpmulmpt  42859  mzpsubst  42865  mzpcong  43089  fnwe2lem2  43168  islmodfg  43186  kercvrlsm  43200  dgrsub2  43252  mpaaeu  43267  rngunsnply  43286  hausgraph  43322  ofoafg  43471  ofoafo  43473  ofoaid1  43475  ofoaid2  43476  naddcnff  43479  naddcnffn  43480  naddcnffo  43481  naddcnfcom  43483  naddcnfid1  43484  naddcnfass  43486  fsovf1od  44133  brcoffn  44147  clsneiel1  44225  wfximgfd  44280  extoimad  44281  mnringmulrcld  44345  mnurndlem1  44398  caofcan  44440  ofmul12  44442  ofdivrec  44443  ofdivcan4  44444  ofdivdiv2  44445  dvconstbi  44451  binomcxplemnotnn0  44473  relpmin  45069  refsum2cnlem1  45158  ssmapsn  45337  preimaiocmnf  45684  fsumsupp0  45702  fsumsermpt  45703  climinf  45730  climinf2lem  45828  limsupmnflem  45842  limsupvaluz2  45860  supcnvlimsup  45862  limsupgtlem  45899  liminfvalxr  45905  liminflelimsupuz  45907  xlimconst2  45957  climxlim2  45968  icccncfext  46009  dvnprodlem1  46068  volicoff  46117  voliooicof  46118  fourierdlem25  46254  etransclem2  46358  etransclem35  46391  fge0iccico  46492  sge0tsms  46502  sge0sup  46513  sge0resrn  46526  sge0le  46529  sge0fodjrnlem  46538  sge0isum  46549  sge0seq  46568  nnfoctbdjlem  46577  meadjiunlem  46587  omeiunle  46639  hoicvr  46670  ovolval4lem1  46771  ovolval5lem3  46776  ovnovollem1  46778  ovnovollem2  46779  iinhoiicclem  46795  iunhoiioolem  46797  preimaicomnf  46833  smfresal  46910  smfsuplem1  46933  smflimsuplem2  46943  fcoreslem3  47189  fcoreslem4  47190  fcores  47191  isubgredg  47990  upgrimpths  48033  ackvalsucsucval  48813  funchomf  49222  imasubc  49276  imassc  49278  imaid  49279  prcofdiag1  49518  prcofdiag  49519  oppfdiag1  49539  oppfdiag  49541  amgmwlem  49927