Theorem ffnd 6652

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 6651	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 6476  ⟶wf 6477

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 6485

This theorem is referenced by:  fnconstg  6711  f1fn  6720  fofn  6737  f1ofn  6764  feqmptd  6890  fssrescdmd  7059  fprb  7128  cocan1  7225  oprres  7514  off  7628  coof  7634  ofco  7635  caofref  7641  caofid0l  7643  caofid0r  7644  caofid1  7645  caofid2  7646  caofrss  7649  caoftrn  7651  fo2ndf  8051  fnwelem  8061  fnse  8063  suppsnop  8108  suppss  8124  suppssr  8125  suppssrg  8126  suppssof1  8129  suppofssd  8133  suppofss1d  8134  suppofss2d  8135  suppcoss  8137  smocdmdom  8288  elmapfn  8789  ralxpmap  8820  omxpenlem  8991  mapen  9054  f1finf1o  9157  unirnffid  9231  fdmfifsupp  9259  mapfien  9292  intrnfi  9300  marypha2  9323  ordtypelem7  9410  wemapsolem  9436  wemapso  9437  wemapso2lem  9438  unxpwdom2  9474  ixpiunwdom  9476  cantnfle  9561  cantnfp1lem2  9569  cantnfp1lem3  9570  cantnfp1  9571  oemapvali  9574  cantnflem1a  9575  cantnflem1c  9577  cantnflem3  9581  cantnf  9583  cnfcomlem  9589  cnfcom3  9594  updjudhcoinlf  9822  updjudhcoinrg  9823  fseqenlem1  9912  numacn  9937  infpwfien  9950  isf32lem2  10242  isf34lem7  10267  isf34lem6  10268  unirnfdomd  10455  ofsubeq0  12119  ofnegsub  12120  ofsubge0  12121  seqf1olem2  13946  resunimafz0  14349  wrdfn  14432  swrdvalfn  14556  pfxfn  14586  pfxid  14589  cats1un  14625  cshwfn  14705  ccatco  14739  limsupgle  15381  o1of2  15517  o1rlimmul  15523  isercolllem2  15570  isercoll  15572  isercoll2  15573  climsup  15574  fsumss  15629  ruclem11  16146  vdwlem2  16891  vdwlem6  16895  vdwlem9  16898  vdwlem12  16901  0ram  16929  ramub1lem1  16935  pwsle  17393  pwsleval  17394  pwsvscaval  17396  mrcuni  17524  mrcun  17525  invf1o  17673  funcres2c  17807  setcmon  17991  setcepi  17992  uncfcurf  18142  yoniso  18188  isacs4lem  18447  acsmapd  18457  chnso  18527  gsumval2  18591  mgmhmf1o  18605  resmgmhm2b  18618  mgmhmima  18620  mgmhmeql  18621  prdsplusgsgrpcl  18637  prdssgrpd  18638  prdsplusgcl  18673  prdsidlem  18674  prdsmndd  18675  mhmf1o  18701  resmhm2b  18727  mhmimalem  18729  mhmima  18730  mhmeql  18731  prdspjmhm  18734  pwsco1mhm  18737  pwsco2mhm  18738  gsumwmhm  18750  frmdss2  18768  grpinvf1o  18919  prdsinvlem  18959  cycsubgcl  19116  ghmrn  19139  ghmpreima  19148  ghmeql  19149  ghmnsgima  19150  ghmnsgpreima  19151  ghmeqker  19153  ghmf1o  19158  ghmqusnsglem1  19190  ghmqusnsg  19192  ghmquskerlem1  19193  ghmquskerco  19194  ghmquskerlem3  19196  ghmqusker  19197  gass  19211  cntzmhm  19251  symgextres  19335  gsmsymgrfixlem1  19337  fvcosymgeq  19339  f1omvdconj  19356  pmtrfinv  19371  symgtrinv  19382  pmtr3ncomlem1  19383  sygbasnfpfi  19422  efginvrel2  19637  efgredleme  19653  ghmplusg  19756  prdscmnd  19771  gsumval3a  19813  gsumval3eu  19814  gsumzaddlem  19831  gsumzsplit  19837  gsumpt  19872  prdsgsum  19891  dprdfcntz  19927  dprdfadd  19932  dprdfeq0  19934  dprdf11  19935  dprdlub  19938  dprdspan  19939  dprd2dlem1  19953  dmdprdpr  19961  dprdpr  19962  dpjlem  19963  ablfac1eu  19985  gsumle  20055  prdsmulrngcl  20091  prdsrngd  20092  prdsringd  20237  prdscrngd  20238  prds1  20239  pwspjmhmmgpd  20244  rnghmf1o  20368  rhmf1o  20406  rhmimasubrnglem  20478  rnrhmsubrg  20518  rrgsupp  20614  imadrhmcl  20710  isabvd  20725  lmodfopnelem1  20829  lcomfsupp  20833  prdsvscacl  20899  prdslmodd  20900  lmhmco  20975  lmhmplusg  20976  lmhmvsca  20977  lmhmf1o  20978  lmhmeql  20987  lspextmo  20988  rhmpreimaidl  21212  pjfo  21650  dsmmbas2  21672  dsmm0cl  21675  dsmmacl  21676  dsmmsubg  21678  dsmmlss  21679  frlmvplusgvalc  21702  frlmvscaval  21703  frlmplusgvalb  21704  frlmvscavalb  21705  frlmsslss2  21710  frlmphllem  21715  frlmphl  21716  frlmssuvc2  21730  frlmsslsp  21731  frlmup1  21733  frlmup2  21734  frlmup3  21735  frlmup4  21736  islindf4  21773  psrbagfsupp  21854  psrbaglesupp  21857  psrbaglecl  21858  psrbagaddcl  21859  psrbagcon  21860  psrbaglefi  21861  psrbagleadd1  21863  psrbagconf1o  21864  gsumbagdiaglem  21865  psrass1lem  21867  psrvscaval  21885  psrlidm  21897  psrridm  21898  psrass1  21899  psrdi  21900  psrdir  21901  psrascl  21914  mvrf2  21928  mplsubglem  21934  mplvscaval  21951  subrgmvrf  21967  mplbas2  21975  mplind  22003  psrbagev1  22010  psrbagev2  22011  evlslem3  22013  evlslem1  22015  evlsvar  22023  mpfind  22040  ismhp3  22055  mhpmulcl  22062  psdmplcl  22075  psdadd  22076  psdvsca  22077  psdmul  22079  psdmvr  22082  psrplusgpropd  22146  coe1add  22176  coe1addfv  22177  evl1addd  22254  evl1subd  22255  evl1muld  22256  pf1mpf  22265  pf1ind  22268  evls1fpws  22282  ressply1evl  22283  rhmply1vsca  22301  mamudir  22317  mamulid  22354  mamurid  22355  mdetrlin  22515  mdetrsca  22516  mdetralt  22521  mdetunilem7  22531  mdetunilem9  22533  madurid  22557  cnrest2  23199  lmss  23211  lmcnp  23217  cnt0  23259  cnt1  23263  cnhaus  23267  rncmp  23309  conncn  23339  2ndcomap  23371  1stccnp  23375  comppfsc  23445  1stckgenlem  23466  ptbasfi  23494  ptopn  23496  ptclsg  23528  ptcnp  23535  upxp  23536  txtube  23553  txcmplem1  23554  hauseqlcld  23559  xkohaus  23566  xkoptsub  23567  cnmpt11  23576  cnmpt21  23584  cnmpt22f  23588  cnmptcom  23591  qtopss  23628  qtopeu  23629  qtopomap  23631  qtopcmap  23632  kqffn  23638  hmeof1o2  23676  xkocnv  23727  rnelfm  23866  ptcmplem1  23965  cnextfres1  23981  ghmcnp  24028  tgphaus  24030  prdstmdd  24037  prdstgpd  24038  fmucnd  24204  psmetxrge0  24226  isxmet2d  24240  prdsmet  24283  blelrnps  24329  blelrn  24330  xmetresbl  24350  comet  24426  stdbdxmet  24428  met2ndci  24435  prdsxmslem2  24442  isngp3  24511  nmotri  24652  metdsre  24767  bndth  24882  evth  24883  fmcfil  25197  bcthlem4  25252  rrxcph  25317  rrxds  25318  rrxmet  25333  evthicc2  25386  ovolfsf  25397  ovolmge0  25403  ovollb2lem  25414  ovolunlem1a  25422  ovoliunlem1  25428  ovoliun  25431  ovoliun2  25432  ovolscalem1  25439  ovolicc1  25442  ovolicc2lem4  25446  ovolicc2  25448  voliunlem1  25476  voliunlem3  25478  volsup  25482  ioombl1lem2  25485  ioombl1lem4  25487  uniiccdif  25504  uniioombllem2  25509  uniioombllem3  25511  uniioombllem6  25514  volsup2  25531  vitalilem4  25537  mbfeqalem1  25567  mbfmulc2lem  25573  mbfmax  25575  mbfaddlem  25586  mbfadd  25587  mbfsub  25588  mbfsup  25590  mbfinf  25591  itg1ge0  25612  itg1addlem1  25618  i1faddlem  25619  i1fmullem  25620  i1fadd  25621  i1fmul  25622  itg1addlem4  25625  i1fmulclem  25628  i1fmulc  25629  itg1mulc  25630  i1fres  25631  itg10a  25636  itg1ge0a  25637  itg1lea  25638  mbfi1fseqlem3  25643  mbfi1fseqlem4  25644  mbfi1flimlem  25648  mbfmullem2  25650  mbfmul  25652  itg20  25663  itg2lea  25670  itg2splitlem  25674  itg2split  25675  itg2monolem1  25676  itg2monolem2  25677  itg2monolem3  25678  itg2mono  25679  itg2i1fseqle  25680  itg2i1fseq  25681  itg2addlem  25684  itg2gt0  25686  itg2cnlem1  25687  itg2cnlem2  25688  itg2cn  25689  itgitg1  25735  bddmulibl  25765  bddibl  25766  dvidlem  25841  dvaddbr  25865  dvmulbr  25866  dvmulbrOLD  25867  dvaddf  25870  dvcmulf  25873  dvrec  25884  dvcnvlem  25905  rolle  25919  dveq0  25930  dv11cn  25931  dvivthlem2  25939  dvivth  25940  dvne0  25941  lhop1lem  25943  lhop1  25944  lhop2  25945  lhop  25946  ftc1cn  25975  tdeglem1  25988  tdeglem3  25989  tdeglem4  25990  mdegleb  25994  mdegldg  25996  mdegaddle  26004  ply1remlem  26095  ply1rem  26096  fta1glem1  26098  fta1glem2  26099  fta1blem  26101  idomrootle  26103  plyeq0lem  26140  plyeq0  26141  plyaddlem1  26143  coeeulem  26154  coeaddlem  26179  coemulc  26185  dgradd2  26199  dgrcolem2  26205  ofmulrt  26214  plyrem  26238  vieta1lem1  26243  vieta1  26245  plyexmo  26246  elqaalem3  26254  aannenlem1  26261  aalioulem2  26266  ulmuni  26326  ulmdvlem1  26334  ulmdv  26337  mbfulm  26340  iblulm  26341  itgulm  26342  rlimcnp2  26901  jensen  26924  amgm  26926  basellem3  27018  basellem7  27022  basellem9  27024  dchrelbas2  27173  dchrmulcl  27185  dchrfi  27191  dchreq  27194  dchrresb  27195  dchrinv  27197  dchr1re  27199  sumdchr2  27206  dchr2sum  27209  lgsqrlem2  27283  lgsqrlem3  27284  rpvmasum2  27448  dchrisum0re  27449  mirf1o  28645  lmif1o  28771  eqeefv  28879  axlowdimlem14  28931  vtxdgfisf  29453  2pthon3v  29919  nvinvfval  30615  sspg  30703  ssps  30705  sspmlem  30707  sspn  30711  lnon0  30773  ubthlem1  30845  pjfn  31684  kbpj  31931  kbass2  32092  elpjrn  32165  ofrn2  32617  off2  32618  ofresid  32619  xppreima2  32628  ofpreima2  32643  suppovss  32657  resf1o  32708  prodindf  32839  indpreima  32841  swrdrn3  32931  pwrssmgc  32976  mgcf1o  32979  gsumfs2d  33030  gsumhashmul  33036  symgcom2  33048  pmtrcnel  33053  pmtrcnel2  33054  pmtrcnelor  33055  cycpmfvlem  33076  cycpmfv3  33079  cycpmcl  33080  cycpmco2rn  33089  cycpmco2  33097  cycpm3cl2  33100  cyc3co2  33104  cyc3evpm  33114  elrgspnlem1  33204  elrgspnlem2  33205  elrgspnlem4  33207  elrgspnsubrunlem1  33209  elrgspnsubrunlem2  33210  gsumind  33305  islinds5  33327  ellspds  33328  elrspunidl  33388  elrspunsn  33389  rhmimaidl  33392  rhmpreimaprmidl  33411  rprmdvdsprod  33494  1arithidomlem2  33496  evls1fn  33518  ply1dg1rt  33538  ply1mulrtss  33540  ply1degltel  33550  ply1degleel  33551  ply1degltlss  33552  ply1gsumz  33554  ig1pmindeg  33557  r1pquslmic  33566  mplvrpmmhm  33571  mplvrpmrhm  33572  esplyfv1  33585  esplyfv  33586  exsslsb  33604  ply1degltdimlem  33630  ply1degltdim  33631  dimkerim  33635  fedgmullem2  33638  fedgmul  33639  lvecendof1f1o  33641  fldextrspunlsplem  33681  fldextrspunlsp  33682  irngss  33695  irngnzply1  33699  extdgfialglem2  33701  irngnminplynz  33720  2sqr3minply  33788  cos9thpiminply  33796  cmpcref  33858  rhmpreimacnlem  33892  fsumcvg4  33958  pl1cn  33963  qqhval2lem  33989  esumcvg  34094  ofcf  34111  ofcof  34115  measfn  34212  meascnbl  34227  sibfof  34348  sitgaddlemb  34356  subiwrdlen  34394  rrvfn  34453  plymul02  34554  signsplypnf  34558  signsply0  34559  reprsuc  34623  reprdifc  34635  breprexplema  34638  circlemethhgt  34651  hgt750lemb  34664  f1resrcmplf1dlem  35093  pthhashvtx  35160  cvmopnlem  35310  cvmliftmolem1  35313  cvmliftlem10  35326  cvmlift2lem9a  35335  cvmlift2lem6  35340  cvmlift2lem12  35346  cvmliftphtlem  35349  cvmlift3lem9  35359  mrsubrn  35545  elmrsubrn  35552  elmsubrn  35560  msubrn  35561  mclsind  35602  mclsppslem  35615  mclspps  35616  iprodefisumlem  35772  weiunfrlem  36497  matunitlindflem1  37655  poimirlem1  37660  poimirlem2  37661  poimirlem3  37662  poimirlem16  37675  poimirlem17  37676  poimirlem19  37678  poimirlem20  37679  poimirlem22  37681  poimirlem23  37682  poimirlem29  37688  poimirlem30  37689  poimirlem31  37690  poimir  37692  mblfinlem2  37697  itg2addnclem3  37712  itg2addnc  37713  itg2gt0cn  37714  ftc1cnnc  37731  ftc1anclem5  37736  ftc1anclem7  37738  ftc1anc  37740  sdclem2  37781  istotbnd3  37810  sstotbnd2  37813  isbnd3  37823  heibor1lem  37848  rrnmet  37868  grpokerinj  37932  isdrngo2  37997  lfl1  39108  lfladdcl  39109  lflvscl  39115  lkr0f  39132  lkrsc  39135  eqlkr2  39138  eqlkr3  39139  ldualvaddval  39169  ldualvsval  39176  tendoeq1  40802  zndvdchrrhm  42004  hashscontpow  42154  aks6d1c3  42155  aks6d1c2lem4  42159  aks6d1c2  42162  sticksstones1  42178  sticksstones2  42179  sticksstones3  42180  sticksstones12a  42189  sticksstones12  42190  aks6d1c6lem2  42203  aks6d1c6lem3  42204  aks6d1c6isolem1  42206  aks6d1c6isolem3  42208  aks6d1c6lem5  42209  aks6d1c7lem1  42212  unitscyglem1  42227  dvun  42391  frlmvscadiccat  42538  fiabv  42568  frlmsnic  42572  pwsgprod  42576  mplmapghm  42588  evlsvvval  42595  evlsaddval  42600  evlsmulval  42601  evladdval  42607  evlmulval  42608  selvvvval  42617  evlselvlem  42618  evlselv  42619  fsuppssind  42625  mhphf  42629  ismrcd1  42730  ismrcd2  42731  istopclsd  42732  isnacs3  42742  mzpaddmpt  42773  mzpmulmpt  42774  mzpsubst  42780  mzpcong  43004  fnwe2lem2  43083  islmodfg  43101  kercvrlsm  43115  dgrsub2  43167  mpaaeu  43182  rngunsnply  43201  hausgraph  43237  ofoafg  43386  ofoafo  43388  ofoaid1  43390  ofoaid2  43391  naddcnff  43394  naddcnffn  43395  naddcnffo  43396  naddcnfcom  43398  naddcnfid1  43399  naddcnfass  43401  fsovf1od  44048  brcoffn  44062  clsneiel1  44140  wfximgfd  44195  extoimad  44196  mnringmulrcld  44260  mnurndlem1  44313  caofcan  44355  ofmul12  44357  ofdivrec  44358  ofdivcan4  44359  ofdivdiv2  44360  dvconstbi  44366  binomcxplemnotnn0  44388  relpmin  44984  refsum2cnlem1  45073  ssmapsn  45252  preimaiocmnf  45599  fsumsupp0  45617  fsumsermpt  45618  climinf  45645  climinf2lem  45743  limsupmnflem  45757  limsupvaluz2  45775  supcnvlimsup  45777  limsupgtlem  45814  liminfvalxr  45820  liminflelimsupuz  45822  xlimconst2  45872  climxlim2  45883  icccncfext  45924  dvnprodlem1  45983  volicoff  46032  voliooicof  46033  fourierdlem25  46169  etransclem2  46273  etransclem35  46306  fge0iccico  46407  sge0tsms  46417  sge0sup  46428  sge0resrn  46441  sge0le  46444  sge0fodjrnlem  46453  sge0isum  46464  sge0seq  46483  nnfoctbdjlem  46492  meadjiunlem  46502  omeiunle  46554  hoicvr  46585  ovolval4lem1  46686  ovolval5lem3  46691  ovnovollem1  46693  ovnovollem2  46694  iinhoiicclem  46710  iunhoiioolem  46712  preimaicomnf  46748  smfresal  46825  smfsuplem1  46848  smflimsuplem2  46858  fcoreslem3  47095  fcoreslem4  47096  fcores  47097  isubgredg  47896  upgrimpths  47939  ackvalsucsucval  48719  funchomf  49128  imasubc  49182  imassc  49184  imaid  49185  prcofdiag1  49424  prcofdiag  49425  oppfdiag1  49445  oppfdiag  49447  amgmwlem  49833