Theorem ffnd 6673

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

Syntax hints:   → wi 4   Fn wfn 6497  ⟶wf 6498

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 6506

This theorem is referenced by:  fnconstg  6732  f1fn  6741  fofn  6758  f1ofn  6785  feqmptd  6912  fssrescdmd  7083  fprb  7152  cocan1  7249  oprres  7538  off  7652  coof  7658  ofco  7659  caofref  7665  caofid0l  7667  caofid0r  7668  caofid1  7669  caofid2  7670  caofrss  7673  caoftrn  7675  fo2ndf  8075  fnwelem  8085  fnse  8087  suppsnop  8132  suppss  8148  suppssr  8149  suppssrg  8150  suppssof1  8153  suppofssd  8157  suppofss1d  8158  suppofss2d  8159  suppcoss  8161  smocdmdom  8312  elmapfn  8816  ralxpmap  8848  omxpenlem  9020  mapen  9083  f1finf1o  9187  unirnffid  9261  fdmfifsupp  9292  mapfien  9325  intrnfi  9333  marypha2  9356  ordtypelem7  9443  wemapsolem  9469  wemapso  9470  wemapso2lem  9471  unxpwdom2  9507  ixpiunwdom  9509  cantnfle  9594  cantnfp1lem2  9602  cantnfp1lem3  9603  cantnfp1  9604  oemapvali  9607  cantnflem1a  9608  cantnflem1c  9610  cantnflem3  9614  cantnf  9616  cnfcomlem  9622  cnfcom3  9627  updjudhcoinlf  9858  updjudhcoinrg  9859  fseqenlem1  9948  numacn  9973  infpwfien  9986  isf32lem2  10278  isf34lem7  10303  isf34lem6  10304  unirnfdomd  10492  ofsubeq0  12156  ofnegsub  12157  ofsubge0  12158  seqf1olem2  13979  resunimafz0  14382  wrdfn  14465  swrdvalfn  14589  pfxfn  14619  pfxid  14622  cats1un  14658  cshwfn  14738  ccatco  14772  limsupgle  15414  o1of2  15550  o1rlimmul  15556  isercolllem2  15603  isercoll  15605  isercoll2  15606  climsup  15607  fsumss  15662  ruclem11  16179  vdwlem2  16924  vdwlem6  16928  vdwlem9  16931  vdwlem12  16934  0ram  16962  ramub1lem1  16968  pwsle  17427  pwsleval  17428  pwsvscaval  17430  mrcuni  17558  mrcun  17559  invf1o  17707  funcres2c  17841  setcmon  18025  setcepi  18026  uncfcurf  18176  yoniso  18222  isacs4lem  18481  acsmapd  18491  chnso  18561  gsumval2  18625  mgmhmf1o  18639  resmgmhm2b  18652  mgmhmima  18654  mgmhmeql  18655  prdsplusgsgrpcl  18671  prdssgrpd  18672  prdsplusgcl  18707  prdsidlem  18708  prdsmndd  18709  mhmf1o  18735  resmhm2b  18761  mhmimalem  18763  mhmima  18764  mhmeql  18765  prdspjmhm  18768  pwsco1mhm  18771  pwsco2mhm  18772  gsumwmhm  18784  frmdss2  18802  grpinvf1o  18956  prdsinvlem  18996  cycsubgcl  19152  ghmrn  19175  ghmpreima  19184  ghmeql  19185  ghmnsgima  19186  ghmnsgpreima  19187  ghmeqker  19189  ghmf1o  19194  ghmqusnsglem1  19226  ghmqusnsg  19228  ghmquskerlem1  19229  ghmquskerco  19230  ghmquskerlem3  19232  ghmqusker  19233  gass  19247  cntzmhm  19287  symgextres  19371  gsmsymgrfixlem1  19373  fvcosymgeq  19375  f1omvdconj  19392  pmtrfinv  19407  symgtrinv  19418  pmtr3ncomlem1  19419  sygbasnfpfi  19458  efginvrel2  19673  efgredleme  19689  ghmplusg  19792  prdscmnd  19807  gsumval3a  19849  gsumval3eu  19850  gsumzaddlem  19867  gsumzsplit  19873  gsumpt  19908  prdsgsum  19927  dprdfcntz  19963  dprdfadd  19968  dprdfeq0  19970  dprdf11  19971  dprdlub  19974  dprdspan  19975  dprd2dlem1  19989  dmdprdpr  19997  dprdpr  19998  dpjlem  19999  ablfac1eu  20021  gsumle  20091  prdsmulrngcl  20127  prdsrngd  20128  prdsringd  20273  prdscrngd  20274  prds1  20275  pwspjmhmmgpd  20280  pwsgprod  20282  rnghmf1o  20405  rhmf1o  20443  rhmimasubrnglem  20515  rnrhmsubrg  20555  rrgsupp  20651  imadrhmcl  20747  isabvd  20762  lmodfopnelem1  20866  lcomfsupp  20870  prdsvscacl  20936  prdslmodd  20937  lmhmco  21012  lmhmplusg  21013  lmhmvsca  21014  lmhmf1o  21015  lmhmeql  21024  lspextmo  21025  rhmpreimaidl  21249  pjfo  21687  dsmmbas2  21709  dsmm0cl  21712  dsmmacl  21713  dsmmsubg  21715  dsmmlss  21716  frlmvplusgvalc  21739  frlmvscaval  21740  frlmplusgvalb  21741  frlmvscavalb  21742  frlmsslss2  21747  frlmphllem  21752  frlmphl  21753  frlmssuvc2  21767  frlmsslsp  21768  frlmup1  21770  frlmup2  21771  frlmup3  21772  frlmup4  21773  islindf4  21810  psrbagfsupp  21892  psrbaglesupp  21895  psrbaglecl  21896  psrbagaddcl  21897  psrbagcon  21898  psrbaglefi  21899  psrbagleadd1  21901  psrbagconf1o  21902  gsumbagdiaglem  21903  psrass1lem  21905  psrvscaval  21923  psrlidm  21934  psrridm  21935  psrass1  21936  psrdi  21937  psrdir  21938  psrascl  21951  mvrf2  21965  mplsubglem  21971  mplvscaval  21988  subrgmvrf  22006  mplbas2  22014  mplind  22042  psrbagev1  22049  psrbagev2  22050  evlslem3  22052  evlslem1  22054  evlsvvval  22065  evlsvar  22067  evladdval  22075  evlmulval  22076  mpfind  22087  ismhp3  22102  mhpmulcl  22109  psdmplcl  22122  psdadd  22123  psdvsca  22124  psdmul  22126  psdmvr  22129  psrplusgpropd  22193  coe1add  22223  coe1addfv  22224  evl1addd  22302  evl1subd  22303  evl1muld  22304  pf1mpf  22313  pf1ind  22316  evls1fpws  22330  ressply1evl  22331  rhmply1vsca  22349  mamudir  22365  mamulid  22402  mamurid  22403  mdetrlin  22563  mdetrsca  22564  mdetralt  22569  mdetunilem7  22579  mdetunilem9  22581  madurid  22605  cnrest2  23247  lmss  23259  lmcnp  23265  cnt0  23307  cnt1  23311  cnhaus  23315  rncmp  23357  conncn  23387  2ndcomap  23419  1stccnp  23423  comppfsc  23493  1stckgenlem  23514  ptbasfi  23542  ptopn  23544  ptclsg  23576  ptcnp  23583  upxp  23584  txtube  23601  txcmplem1  23602  hauseqlcld  23607  xkohaus  23614  xkoptsub  23615  cnmpt11  23624  cnmpt21  23632  cnmpt22f  23636  cnmptcom  23639  qtopss  23676  qtopeu  23677  qtopomap  23679  qtopcmap  23680  kqffn  23686  hmeof1o2  23724  xkocnv  23775  rnelfm  23914  ptcmplem1  24013  cnextfres1  24029  ghmcnp  24076  tgphaus  24078  prdstmdd  24085  prdstgpd  24086  fmucnd  24252  psmetxrge0  24274  isxmet2d  24288  prdsmet  24331  blelrnps  24377  blelrn  24378  xmetresbl  24398  comet  24474  stdbdxmet  24476  met2ndci  24483  prdsxmslem2  24490  isngp3  24559  nmotri  24700  metdsre  24815  bndth  24930  evth  24931  fmcfil  25245  bcthlem4  25300  rrxcph  25365  rrxds  25366  rrxmet  25381  evthicc2  25434  ovolfsf  25445  ovolmge0  25451  ovollb2lem  25462  ovolunlem1a  25470  ovoliunlem1  25476  ovoliun  25479  ovoliun2  25480  ovolscalem1  25487  ovolicc1  25490  ovolicc2lem4  25494  ovolicc2  25496  voliunlem1  25524  voliunlem3  25526  volsup  25530  ioombl1lem2  25533  ioombl1lem4  25535  uniiccdif  25552  uniioombllem2  25557  uniioombllem3  25559  uniioombllem6  25562  volsup2  25579  vitalilem4  25585  mbfeqalem1  25615  mbfmulc2lem  25621  mbfmax  25623  mbfaddlem  25634  mbfadd  25635  mbfsub  25636  mbfsup  25638  mbfinf  25639  itg1ge0  25660  itg1addlem1  25666  i1faddlem  25667  i1fmullem  25668  i1fadd  25669  i1fmul  25670  itg1addlem4  25673  i1fmulclem  25676  i1fmulc  25677  itg1mulc  25678  i1fres  25679  itg10a  25684  itg1ge0a  25685  itg1lea  25686  mbfi1fseqlem3  25691  mbfi1fseqlem4  25692  mbfi1flimlem  25696  mbfmullem2  25698  mbfmul  25700  itg20  25711  itg2lea  25718  itg2splitlem  25722  itg2split  25723  itg2monolem1  25724  itg2monolem2  25725  itg2monolem3  25726  itg2mono  25727  itg2i1fseqle  25728  itg2i1fseq  25729  itg2addlem  25732  itg2gt0  25734  itg2cnlem1  25735  itg2cnlem2  25736  itg2cn  25737  itgitg1  25783  bddmulibl  25813  bddibl  25814  dvidlem  25889  dvaddbr  25913  dvmulbr  25914  dvmulbrOLD  25915  dvaddf  25918  dvcmulf  25921  dvrec  25932  dvcnvlem  25953  rolle  25967  dveq0  25978  dv11cn  25979  dvivthlem2  25987  dvivth  25988  dvne0  25989  lhop1lem  25991  lhop1  25992  lhop2  25993  lhop  25994  ftc1cn  26023  tdeglem1  26036  tdeglem3  26037  tdeglem4  26038  mdegleb  26042  mdegldg  26044  mdegaddle  26052  ply1remlem  26143  ply1rem  26144  fta1glem1  26146  fta1glem2  26147  fta1blem  26149  idomrootle  26151  plyeq0lem  26188  plyeq0  26189  plyaddlem1  26191  coeeulem  26202  coeaddlem  26227  coemulc  26233  dgradd2  26247  dgrcolem2  26253  ofmulrt  26262  plyrem  26286  vieta1lem1  26291  vieta1  26293  plyexmo  26294  elqaalem3  26302  aannenlem1  26309  aalioulem2  26314  ulmuni  26374  ulmdvlem1  26382  ulmdv  26385  mbfulm  26388  iblulm  26389  itgulm  26390  rlimcnp2  26949  jensen  26972  amgm  26974  basellem3  27066  basellem7  27070  basellem9  27072  dchrelbas2  27221  dchrmulcl  27233  dchrfi  27239  dchreq  27242  dchrresb  27243  dchrinv  27245  dchr1re  27247  sumdchr2  27254  dchr2sum  27257  lgsqrlem2  27331  lgsqrlem3  27332  rpvmasum2  27496  dchrisum0re  27497  mirf1o  28759  lmif1o  28885  eqeefv  28994  axlowdimlem14  29046  vtxdgfisf  29568  2pthon3v  30034  nvinvfval  30734  sspg  30822  ssps  30824  sspmlem  30826  sspn  30830  lnon0  30892  ubthlem1  30964  pjfn  31803  kbpj  32050  kbass2  32211  elpjrn  32284  ofrn2  32736  off2  32737  ofresid  32738  xppreima2  32747  ofpreima2  32762  suppovss  32777  resf1o  32826  prodindf  32961  indpreima  32964  swrdrn3  33054  pwrssmgc  33099  mgcf1o  33102  gsumfs2d  33161  gsumhashmul  33167  symgcom2  33184  pmtrcnel  33189  pmtrcnel2  33190  pmtrcnelor  33191  cycpmfvlem  33212  cycpmfv3  33215  cycpmcl  33216  cycpmco2rn  33225  cycpmco2  33233  cycpm3cl2  33236  cyc3co2  33240  cyc3evpm  33250  elrgspnlem1  33342  elrgspnlem2  33343  elrgspnlem4  33345  elrgspnsubrunlem1  33347  elrgspnsubrunlem2  33348  gsumind  33444  islinds5  33466  ellspds  33467  elrspunidl  33527  elrspunsn  33528  rhmimaidl  33531  rhmpreimaprmidl  33550  rprmdvdsprod  33633  1arithidomlem2  33635  evls1fn  33659  ply1dg1rt  33679  ply1mulrtss  33681  ply1degltel  33693  ply1degleel  33694  ply1degltlss  33695  ply1gsumz  33698  ig1pmindeg  33701  r1pquslmic  33710  extvfvcl  33719  mplmulmvr  33722  evlextv  33725  mplvrpmmhm  33729  mplvrpmrhm  33730  psrmonprod  33735  esplyfval0  33747  esplyfval2  33748  esplyfv1  33752  esplyfv  33753  esplyfval3  33755  esplyfvaln  33757  esplyind  33758  vieta  33763  exsslsb  33780  ply1degltdimlem  33806  ply1degltdim  33807  dimkerim  33811  fedgmullem2  33814  fedgmul  33815  lvecendof1f1o  33817  fldextrspunlsplem  33857  fldextrspunlsp  33858  irngss  33871  irngnzply1  33875  extdgfialglem2  33877  irngnminplynz  33896  2sqr3minply  33964  cos9thpiminply  33972  cmpcref  34034  rhmpreimacnlem  34068  fsumcvg4  34134  pl1cn  34139  qqhval2lem  34165  esumcvg  34270  ofcf  34287  ofcof  34291  measfn  34388  meascnbl  34403  sibfof  34524  sitgaddlemb  34532  subiwrdlen  34570  rrvfn  34629  plymul02  34730  signsplypnf  34734  signsply0  34735  reprsuc  34799  reprdifc  34811  breprexplema  34814  circlemethhgt  34827  hgt750lemb  34840  f1resrcmplf1dlem  35269  pthhashvtx  35350  cvmopnlem  35500  cvmliftmolem1  35503  cvmliftlem10  35516  cvmlift2lem9a  35525  cvmlift2lem6  35530  cvmlift2lem12  35536  cvmliftphtlem  35539  cvmlift3lem9  35549  mrsubrn  35735  elmrsubrn  35742  elmsubrn  35750  msubrn  35751  mclsind  35792  mclsppslem  35805  mclspps  35806  iprodefisumlem  35962  weiunfrlem  36686  matunitlindflem1  37896  poimirlem1  37901  poimirlem2  37902  poimirlem3  37903  poimirlem16  37916  poimirlem17  37917  poimirlem19  37919  poimirlem20  37920  poimirlem22  37922  poimirlem23  37923  poimirlem29  37929  poimirlem30  37930  poimirlem31  37931  poimir  37933  mblfinlem2  37938  itg2addnclem3  37953  itg2addnc  37954  itg2gt0cn  37955  ftc1cnnc  37972  ftc1anclem5  37977  ftc1anclem7  37979  ftc1anc  37981  sdclem2  38022  istotbnd3  38051  sstotbnd2  38054  isbnd3  38064  heibor1lem  38089  rrnmet  38109  grpokerinj  38173  isdrngo2  38238  lfl1  39475  lfladdcl  39476  lflvscl  39482  lkr0f  39499  lkrsc  39502  eqlkr2  39505  eqlkr3  39506  ldualvaddval  39536  ldualvsval  39543  tendoeq1  41169  zndvdchrrhm  42371  hashscontpow  42521  aks6d1c3  42522  aks6d1c2lem4  42526  aks6d1c2  42529  sticksstones1  42545  sticksstones2  42546  sticksstones3  42547  sticksstones12a  42556  sticksstones12  42557  aks6d1c6lem2  42570  aks6d1c6lem3  42571  aks6d1c6isolem1  42573  aks6d1c6isolem3  42575  aks6d1c6lem5  42576  aks6d1c7lem1  42579  unitscyglem1  42594  dvun  42758  frlmvscadiccat  42905  fiabv  42935  frlmsnic  42939  mplmapghm  42951  evlsaddval  42958  evlsmulval  42959  selvvvval  42972  evlselvlem  42973  evlselv  42974  fsuppssind  42980  mhphf  42984  ismrcd1  43084  ismrcd2  43085  istopclsd  43086  isnacs3  43096  mzpaddmpt  43127  mzpmulmpt  43128  mzpsubst  43134  mzpcong  43358  fnwe2lem2  43437  islmodfg  43455  kercvrlsm  43469  dgrsub2  43521  mpaaeu  43536  rngunsnply  43555  hausgraph  43591  ofoafg  43740  ofoafo  43742  ofoaid1  43744  ofoaid2  43745  naddcnff  43748  naddcnffn  43749  naddcnffo  43750  naddcnfcom  43752  naddcnfid1  43753  naddcnfass  43755  fsovf1od  44401  brcoffn  44415  clsneiel1  44493  wfximgfd  44548  extoimad  44549  mnringmulrcld  44613  mnurndlem1  44666  caofcan  44708  ofmul12  44710  ofdivrec  44711  ofdivcan4  44712  ofdivdiv2  44713  dvconstbi  44719  binomcxplemnotnn0  44741  relpmin  45337  refsum2cnlem1  45426  ssmapsn  45603  preimaiocmnf  45949  fsumsupp0  45967  fsumsermpt  45968  climinf  45995  climinf2lem  46093  limsupmnflem  46107  limsupvaluz2  46125  supcnvlimsup  46127  limsupgtlem  46164  liminfvalxr  46170  liminflelimsupuz  46172  xlimconst2  46222  climxlim2  46233  icccncfext  46274  dvnprodlem1  46333  volicoff  46382  voliooicof  46383  fourierdlem25  46519  etransclem2  46623  etransclem35  46656  fge0iccico  46757  sge0tsms  46767  sge0sup  46778  sge0resrn  46791  sge0le  46794  sge0fodjrnlem  46803  sge0isum  46814  sge0seq  46833  nnfoctbdjlem  46842  meadjiunlem  46852  omeiunle  46904  hoicvr  46935  ovolval4lem1  47036  ovolval5lem3  47041  ovnovollem1  47043  ovnovollem2  47044  iinhoiicclem  47060  iunhoiioolem  47062  preimaicomnf  47098  smfresal  47175  smfsuplem1  47198  smflimsuplem2  47208  fcoreslem3  47454  fcoreslem4  47455  fcores  47456  isubgredg  48255  upgrimpths  48298  ackvalsucsucval  49077  funchomf  49485  imasubc  49539  imassc  49541  imaid  49542  prcofdiag1  49781  prcofdiag  49782  oppfdiag1  49802  oppfdiag  49804  amgmwlem  50190