Theorem ffnd 6663

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

Syntax hints:   → wi 4   Fn wfn 6487  ⟶wf 6488

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 6496

This theorem is referenced by:  fnconstg  6722  f1fn  6731  fofn  6748  f1ofn  6775  feqmptd  6902  fssrescdmd  7071  fprb  7140  cocan1  7237  oprres  7526  off  7640  coof  7646  ofco  7647  caofref  7653  caofid0l  7655  caofid0r  7656  caofid1  7657  caofid2  7658  caofrss  7661  caoftrn  7663  fo2ndf  8063  fnwelem  8073  fnse  8075  suppsnop  8120  suppss  8136  suppssr  8137  suppssrg  8138  suppssof1  8141  suppofssd  8145  suppofss1d  8146  suppofss2d  8147  suppcoss  8149  smocdmdom  8300  elmapfn  8802  ralxpmap  8834  omxpenlem  9006  mapen  9069  f1finf1o  9173  unirnffid  9247  fdmfifsupp  9278  mapfien  9311  intrnfi  9319  marypha2  9342  ordtypelem7  9429  wemapsolem  9455  wemapso  9456  wemapso2lem  9457  unxpwdom2  9493  ixpiunwdom  9495  cantnfle  9580  cantnfp1lem2  9588  cantnfp1lem3  9589  cantnfp1  9590  oemapvali  9593  cantnflem1a  9594  cantnflem1c  9596  cantnflem3  9600  cantnf  9602  cnfcomlem  9608  cnfcom3  9613  updjudhcoinlf  9844  updjudhcoinrg  9845  fseqenlem1  9934  numacn  9959  infpwfien  9972  isf32lem2  10264  isf34lem7  10289  isf34lem6  10290  unirnfdomd  10478  ofsubeq0  12142  ofnegsub  12143  ofsubge0  12144  seqf1olem2  13965  resunimafz0  14368  wrdfn  14451  swrdvalfn  14575  pfxfn  14605  pfxid  14608  cats1un  14644  cshwfn  14724  ccatco  14758  limsupgle  15400  o1of2  15536  o1rlimmul  15542  isercolllem2  15589  isercoll  15591  isercoll2  15592  climsup  15593  fsumss  15648  ruclem11  16165  vdwlem2  16910  vdwlem6  16914  vdwlem9  16917  vdwlem12  16920  0ram  16948  ramub1lem1  16954  pwsle  17413  pwsleval  17414  pwsvscaval  17416  mrcuni  17544  mrcun  17545  invf1o  17693  funcres2c  17827  setcmon  18011  setcepi  18012  uncfcurf  18162  yoniso  18208  isacs4lem  18467  acsmapd  18477  chnso  18547  gsumval2  18611  mgmhmf1o  18625  resmgmhm2b  18638  mgmhmima  18640  mgmhmeql  18641  prdsplusgsgrpcl  18657  prdssgrpd  18658  prdsplusgcl  18693  prdsidlem  18694  prdsmndd  18695  mhmf1o  18721  resmhm2b  18747  mhmimalem  18749  mhmima  18750  mhmeql  18751  prdspjmhm  18754  pwsco1mhm  18757  pwsco2mhm  18758  gsumwmhm  18770  frmdss2  18788  grpinvf1o  18939  prdsinvlem  18979  cycsubgcl  19135  ghmrn  19158  ghmpreima  19167  ghmeql  19168  ghmnsgima  19169  ghmnsgpreima  19170  ghmeqker  19172  ghmf1o  19177  ghmqusnsglem1  19209  ghmqusnsg  19211  ghmquskerlem1  19212  ghmquskerco  19213  ghmquskerlem3  19215  ghmqusker  19216  gass  19230  cntzmhm  19270  symgextres  19354  gsmsymgrfixlem1  19356  fvcosymgeq  19358  f1omvdconj  19375  pmtrfinv  19390  symgtrinv  19401  pmtr3ncomlem1  19402  sygbasnfpfi  19441  efginvrel2  19656  efgredleme  19672  ghmplusg  19775  prdscmnd  19790  gsumval3a  19832  gsumval3eu  19833  gsumzaddlem  19850  gsumzsplit  19856  gsumpt  19891  prdsgsum  19910  dprdfcntz  19946  dprdfadd  19951  dprdfeq0  19953  dprdf11  19954  dprdlub  19957  dprdspan  19958  dprd2dlem1  19972  dmdprdpr  19980  dprdpr  19981  dpjlem  19982  ablfac1eu  20004  gsumle  20074  prdsmulrngcl  20110  prdsrngd  20111  prdsringd  20256  prdscrngd  20257  prds1  20258  pwspjmhmmgpd  20263  pwsgprod  20265  rnghmf1o  20388  rhmf1o  20426  rhmimasubrnglem  20498  rnrhmsubrg  20538  rrgsupp  20634  imadrhmcl  20730  isabvd  20745  lmodfopnelem1  20849  lcomfsupp  20853  prdsvscacl  20919  prdslmodd  20920  lmhmco  20995  lmhmplusg  20996  lmhmvsca  20997  lmhmf1o  20998  lmhmeql  21007  lspextmo  21008  rhmpreimaidl  21232  pjfo  21670  dsmmbas2  21692  dsmm0cl  21695  dsmmacl  21696  dsmmsubg  21698  dsmmlss  21699  frlmvplusgvalc  21722  frlmvscaval  21723  frlmplusgvalb  21724  frlmvscavalb  21725  frlmsslss2  21730  frlmphllem  21735  frlmphl  21736  frlmssuvc2  21750  frlmsslsp  21751  frlmup1  21753  frlmup2  21754  frlmup3  21755  frlmup4  21756  islindf4  21793  psrbagfsupp  21875  psrbaglesupp  21878  psrbaglecl  21879  psrbagaddcl  21880  psrbagcon  21881  psrbaglefi  21882  psrbagleadd1  21884  psrbagconf1o  21885  gsumbagdiaglem  21886  psrass1lem  21888  psrvscaval  21906  psrlidm  21917  psrridm  21918  psrass1  21919  psrdi  21920  psrdir  21921  psrascl  21934  mvrf2  21948  mplsubglem  21954  mplvscaval  21971  subrgmvrf  21989  mplbas2  21997  mplind  22025  psrbagev1  22032  psrbagev2  22033  evlslem3  22035  evlslem1  22037  evlsvvval  22048  evlsvar  22050  evladdval  22058  evlmulval  22059  mpfind  22070  ismhp3  22085  mhpmulcl  22092  psdmplcl  22105  psdadd  22106  psdvsca  22107  psdmul  22109  psdmvr  22112  psrplusgpropd  22176  coe1add  22206  coe1addfv  22207  evl1addd  22285  evl1subd  22286  evl1muld  22287  pf1mpf  22296  pf1ind  22299  evls1fpws  22313  ressply1evl  22314  rhmply1vsca  22332  mamudir  22348  mamulid  22385  mamurid  22386  mdetrlin  22546  mdetrsca  22547  mdetralt  22552  mdetunilem7  22562  mdetunilem9  22564  madurid  22588  cnrest2  23230  lmss  23242  lmcnp  23248  cnt0  23290  cnt1  23294  cnhaus  23298  rncmp  23340  conncn  23370  2ndcomap  23402  1stccnp  23406  comppfsc  23476  1stckgenlem  23497  ptbasfi  23525  ptopn  23527  ptclsg  23559  ptcnp  23566  upxp  23567  txtube  23584  txcmplem1  23585  hauseqlcld  23590  xkohaus  23597  xkoptsub  23598  cnmpt11  23607  cnmpt21  23615  cnmpt22f  23619  cnmptcom  23622  qtopss  23659  qtopeu  23660  qtopomap  23662  qtopcmap  23663  kqffn  23669  hmeof1o2  23707  xkocnv  23758  rnelfm  23897  ptcmplem1  23996  cnextfres1  24012  ghmcnp  24059  tgphaus  24061  prdstmdd  24068  prdstgpd  24069  fmucnd  24235  psmetxrge0  24257  isxmet2d  24271  prdsmet  24314  blelrnps  24360  blelrn  24361  xmetresbl  24381  comet  24457  stdbdxmet  24459  met2ndci  24466  prdsxmslem2  24473  isngp3  24542  nmotri  24683  metdsre  24798  bndth  24913  evth  24914  fmcfil  25228  bcthlem4  25283  rrxcph  25348  rrxds  25349  rrxmet  25364  evthicc2  25417  ovolfsf  25428  ovolmge0  25434  ovollb2lem  25445  ovolunlem1a  25453  ovoliunlem1  25459  ovoliun  25462  ovoliun2  25463  ovolscalem1  25470  ovolicc1  25473  ovolicc2lem4  25477  ovolicc2  25479  voliunlem1  25507  voliunlem3  25509  volsup  25513  ioombl1lem2  25516  ioombl1lem4  25518  uniiccdif  25535  uniioombllem2  25540  uniioombllem3  25542  uniioombllem6  25545  volsup2  25562  vitalilem4  25568  mbfeqalem1  25598  mbfmulc2lem  25604  mbfmax  25606  mbfaddlem  25617  mbfadd  25618  mbfsub  25619  mbfsup  25621  mbfinf  25622  itg1ge0  25643  itg1addlem1  25649  i1faddlem  25650  i1fmullem  25651  i1fadd  25652  i1fmul  25653  itg1addlem4  25656  i1fmulclem  25659  i1fmulc  25660  itg1mulc  25661  i1fres  25662  itg10a  25667  itg1ge0a  25668  itg1lea  25669  mbfi1fseqlem3  25674  mbfi1fseqlem4  25675  mbfi1flimlem  25679  mbfmullem2  25681  mbfmul  25683  itg20  25694  itg2lea  25701  itg2splitlem  25705  itg2split  25706  itg2monolem1  25707  itg2monolem2  25708  itg2monolem3  25709  itg2mono  25710  itg2i1fseqle  25711  itg2i1fseq  25712  itg2addlem  25715  itg2gt0  25717  itg2cnlem1  25718  itg2cnlem2  25719  itg2cn  25720  itgitg1  25766  bddmulibl  25796  bddibl  25797  dvidlem  25872  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  dvaddf  25901  dvcmulf  25904  dvrec  25915  dvcnvlem  25936  rolle  25950  dveq0  25961  dv11cn  25962  dvivthlem2  25970  dvivth  25971  dvne0  25972  lhop1lem  25974  lhop1  25975  lhop2  25976  lhop  25977  ftc1cn  26006  tdeglem1  26019  tdeglem3  26020  tdeglem4  26021  mdegleb  26025  mdegldg  26027  mdegaddle  26035  ply1remlem  26126  ply1rem  26127  fta1glem1  26129  fta1glem2  26130  fta1blem  26132  idomrootle  26134  plyeq0lem  26171  plyeq0  26172  plyaddlem1  26174  coeeulem  26185  coeaddlem  26210  coemulc  26216  dgradd2  26230  dgrcolem2  26236  ofmulrt  26245  plyrem  26269  vieta1lem1  26274  vieta1  26276  plyexmo  26277  elqaalem3  26285  aannenlem1  26292  aalioulem2  26297  ulmuni  26357  ulmdvlem1  26365  ulmdv  26368  mbfulm  26371  iblulm  26372  itgulm  26373  rlimcnp2  26932  jensen  26955  amgm  26957  basellem3  27049  basellem7  27053  basellem9  27055  dchrelbas2  27204  dchrmulcl  27216  dchrfi  27222  dchreq  27225  dchrresb  27226  dchrinv  27228  dchr1re  27230  sumdchr2  27237  dchr2sum  27240  lgsqrlem2  27314  lgsqrlem3  27315  rpvmasum2  27479  dchrisum0re  27480  mirf1o  28741  lmif1o  28867  eqeefv  28976  axlowdimlem14  29028  vtxdgfisf  29550  2pthon3v  30016  nvinvfval  30715  sspg  30803  ssps  30805  sspmlem  30807  sspn  30811  lnon0  30873  ubthlem1  30945  pjfn  31784  kbpj  32031  kbass2  32192  elpjrn  32265  ofrn2  32718  off2  32719  ofresid  32720  xppreima2  32729  ofpreima2  32744  suppovss  32760  resf1o  32809  prodindf  32944  indpreima  32947  swrdrn3  33037  pwrssmgc  33082  mgcf1o  33085  gsumfs2d  33144  gsumhashmul  33150  symgcom2  33166  pmtrcnel  33171  pmtrcnel2  33172  pmtrcnelor  33173  cycpmfvlem  33194  cycpmfv3  33197  cycpmcl  33198  cycpmco2rn  33207  cycpmco2  33215  cycpm3cl2  33218  cyc3co2  33222  cyc3evpm  33232  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem4  33327  elrgspnsubrunlem1  33329  elrgspnsubrunlem2  33330  gsumind  33426  islinds5  33448  ellspds  33449  elrspunidl  33509  elrspunsn  33510  rhmimaidl  33513  rhmpreimaprmidl  33532  rprmdvdsprod  33615  1arithidomlem2  33617  evls1fn  33641  ply1dg1rt  33661  ply1mulrtss  33663  ply1degltel  33675  ply1degleel  33676  ply1degltlss  33677  ply1gsumz  33680  ig1pmindeg  33683  r1pquslmic  33692  extvfvcl  33701  mplmulmvr  33704  evlextv  33707  mplvrpmmhm  33711  mplvrpmrhm  33712  esplyfval0  33722  esplyfval2  33723  esplyfv1  33727  esplyfv  33728  esplyfval3  33730  esplyind  33731  vieta  33736  exsslsb  33753  ply1degltdimlem  33779  ply1degltdim  33780  dimkerim  33784  fedgmullem2  33787  fedgmul  33788  lvecendof1f1o  33790  fldextrspunlsplem  33830  fldextrspunlsp  33831  irngss  33844  irngnzply1  33848  extdgfialglem2  33850  irngnminplynz  33869  2sqr3minply  33937  cos9thpiminply  33945  cmpcref  34007  rhmpreimacnlem  34041  fsumcvg4  34107  pl1cn  34112  qqhval2lem  34138  esumcvg  34243  ofcf  34260  ofcof  34264  measfn  34361  meascnbl  34376  sibfof  34497  sitgaddlemb  34505  subiwrdlen  34543  rrvfn  34602  plymul02  34703  signsplypnf  34707  signsply0  34708  reprsuc  34772  reprdifc  34784  breprexplema  34787  circlemethhgt  34800  hgt750lemb  34813  f1resrcmplf1dlem  35242  pthhashvtx  35322  cvmopnlem  35472  cvmliftmolem1  35475  cvmliftlem10  35488  cvmlift2lem9a  35497  cvmlift2lem6  35502  cvmlift2lem12  35508  cvmliftphtlem  35511  cvmlift3lem9  35521  mrsubrn  35707  elmrsubrn  35714  elmsubrn  35722  msubrn  35723  mclsind  35764  mclsppslem  35777  mclspps  35778  iprodefisumlem  35934  weiunfrlem  36658  matunitlindflem1  37813  poimirlem1  37818  poimirlem2  37819  poimirlem3  37820  poimirlem16  37833  poimirlem17  37834  poimirlem19  37836  poimirlem20  37837  poimirlem22  37839  poimirlem23  37840  poimirlem29  37846  poimirlem30  37847  poimirlem31  37848  poimir  37850  mblfinlem2  37855  itg2addnclem3  37870  itg2addnc  37871  itg2gt0cn  37872  ftc1cnnc  37889  ftc1anclem5  37894  ftc1anclem7  37896  ftc1anc  37898  sdclem2  37939  istotbnd3  37968  sstotbnd2  37971  isbnd3  37981  heibor1lem  38006  rrnmet  38026  grpokerinj  38090  isdrngo2  38155  lfl1  39326  lfladdcl  39327  lflvscl  39333  lkr0f  39350  lkrsc  39353  eqlkr2  39356  eqlkr3  39357  ldualvaddval  39387  ldualvsval  39394  tendoeq1  41020  zndvdchrrhm  42222  hashscontpow  42372  aks6d1c3  42373  aks6d1c2lem4  42377  aks6d1c2  42380  sticksstones1  42396  sticksstones2  42397  sticksstones3  42398  sticksstones12a  42407  sticksstones12  42408  aks6d1c6lem2  42421  aks6d1c6lem3  42422  aks6d1c6isolem1  42424  aks6d1c6isolem3  42426  aks6d1c6lem5  42427  aks6d1c7lem1  42430  unitscyglem1  42445  dvun  42610  frlmvscadiccat  42757  fiabv  42787  frlmsnic  42791  mplmapghm  42803  evlsaddval  42810  evlsmulval  42811  selvvvval  42824  evlselvlem  42825  evlselv  42826  fsuppssind  42832  mhphf  42836  ismrcd1  42936  ismrcd2  42937  istopclsd  42938  isnacs3  42948  mzpaddmpt  42979  mzpmulmpt  42980  mzpsubst  42986  mzpcong  43210  fnwe2lem2  43289  islmodfg  43307  kercvrlsm  43321  dgrsub2  43373  mpaaeu  43388  rngunsnply  43407  hausgraph  43443  ofoafg  43592  ofoafo  43594  ofoaid1  43596  ofoaid2  43597  naddcnff  43600  naddcnffn  43601  naddcnffo  43602  naddcnfcom  43604  naddcnfid1  43605  naddcnfass  43607  fsovf1od  44253  brcoffn  44267  clsneiel1  44345  wfximgfd  44400  extoimad  44401  mnringmulrcld  44465  mnurndlem1  44518  caofcan  44560  ofmul12  44562  ofdivrec  44563  ofdivcan4  44564  ofdivdiv2  44565  dvconstbi  44571  binomcxplemnotnn0  44593  relpmin  45189  refsum2cnlem1  45278  ssmapsn  45456  preimaiocmnf  45802  fsumsupp0  45820  fsumsermpt  45821  climinf  45848  climinf2lem  45946  limsupmnflem  45960  limsupvaluz2  45978  supcnvlimsup  45980  limsupgtlem  46017  liminfvalxr  46023  liminflelimsupuz  46025  xlimconst2  46075  climxlim2  46086  icccncfext  46127  dvnprodlem1  46186  volicoff  46235  voliooicof  46236  fourierdlem25  46372  etransclem2  46476  etransclem35  46509  fge0iccico  46610  sge0tsms  46620  sge0sup  46631  sge0resrn  46644  sge0le  46647  sge0fodjrnlem  46656  sge0isum  46667  sge0seq  46686  nnfoctbdjlem  46695  meadjiunlem  46705  omeiunle  46757  hoicvr  46788  ovolval4lem1  46889  ovolval5lem3  46894  ovnovollem1  46896  ovnovollem2  46897  iinhoiicclem  46913  iunhoiioolem  46915  preimaicomnf  46951  smfresal  47028  smfsuplem1  47051  smflimsuplem2  47061  fcoreslem3  47307  fcoreslem4  47308  fcores  47309  isubgredg  48108  upgrimpths  48151  ackvalsucsucval  48930  funchomf  49338  imasubc  49392  imassc  49394  imaid  49395  prcofdiag1  49634  prcofdiag  49635  oppfdiag1  49655  oppfdiag  49657  amgmwlem  50043