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  7073  fprb  7142  cocan1  7239  oprres  7528  off  7642  coof  7648  ofco  7649  caofref  7655  caofid0l  7657  caofid0r  7658  caofid1  7659  caofid2  7660  caofrss  7663  caoftrn  7665  fo2ndf  8064  fnwelem  8074  fnse  8076  suppsnop  8121  suppss  8137  suppssr  8138  suppssrg  8139  suppssof1  8142  suppofssd  8146  suppofss1d  8147  suppofss2d  8148  suppcoss  8150  smocdmdom  8301  elmapfn  8805  ralxpmap  8837  omxpenlem  9009  mapen  9072  f1finf1o  9176  unirnffid  9250  fdmfifsupp  9281  mapfien  9314  intrnfi  9322  marypha2  9345  ordtypelem7  9432  wemapsolem  9458  wemapso  9459  wemapso2lem  9460  unxpwdom2  9496  ixpiunwdom  9498  cantnfle  9583  cantnfp1lem2  9591  cantnfp1lem3  9592  cantnfp1  9593  oemapvali  9596  cantnflem1a  9597  cantnflem1c  9599  cantnflem3  9603  cantnf  9605  cnfcomlem  9611  cnfcom3  9616  updjudhcoinlf  9847  updjudhcoinrg  9848  fseqenlem1  9937  numacn  9962  infpwfien  9975  isf32lem2  10267  isf34lem7  10292  isf34lem6  10293  unirnfdomd  10481  ofsubeq0  12147  ofnegsub  12148  ofsubge0  12149  seqf1olem2  13995  resunimafz0  14398  wrdfn  14481  swrdvalfn  14605  pfxfn  14635  pfxid  14638  cats1un  14674  cshwfn  14754  ccatco  14788  limsupgle  15430  o1of2  15566  o1rlimmul  15572  isercolllem2  15619  isercoll  15621  isercoll2  15622  climsup  15623  fsumss  15678  ruclem11  16198  vdwlem2  16944  vdwlem6  16948  vdwlem9  16951  vdwlem12  16954  0ram  16982  ramub1lem1  16988  pwsle  17447  pwsleval  17448  pwsvscaval  17450  mrcuni  17578  mrcun  17579  invf1o  17727  funcres2c  17861  setcmon  18045  setcepi  18046  uncfcurf  18196  yoniso  18242  isacs4lem  18501  acsmapd  18511  chnso  18581  gsumval2  18645  mgmhmf1o  18659  resmgmhm2b  18672  mgmhmima  18674  mgmhmeql  18675  prdsplusgsgrpcl  18691  prdssgrpd  18692  prdsplusgcl  18727  prdsidlem  18728  prdsmndd  18729  mhmf1o  18755  resmhm2b  18781  mhmimalem  18783  mhmima  18784  mhmeql  18785  prdspjmhm  18788  pwsco1mhm  18791  pwsco2mhm  18792  gsumwmhm  18804  frmdss2  18822  grpinvf1o  18976  prdsinvlem  19016  cycsubgcl  19172  ghmrn  19195  ghmpreima  19204  ghmeql  19205  ghmnsgima  19206  ghmnsgpreima  19207  ghmeqker  19209  ghmf1o  19214  ghmqusnsglem1  19246  ghmqusnsg  19248  ghmquskerlem1  19249  ghmquskerco  19250  ghmquskerlem3  19252  ghmqusker  19253  gass  19267  cntzmhm  19307  symgextres  19391  gsmsymgrfixlem1  19393  fvcosymgeq  19395  f1omvdconj  19412  pmtrfinv  19427  symgtrinv  19438  pmtr3ncomlem1  19439  sygbasnfpfi  19478  efginvrel2  19693  efgredleme  19709  ghmplusg  19812  prdscmnd  19827  gsumval3a  19869  gsumval3eu  19870  gsumzaddlem  19887  gsumzsplit  19893  gsumpt  19928  prdsgsum  19947  dprdfcntz  19983  dprdfadd  19988  dprdfeq0  19990  dprdf11  19991  dprdlub  19994  dprdspan  19995  dprd2dlem1  20009  dmdprdpr  20017  dprdpr  20018  dpjlem  20019  ablfac1eu  20041  gsumle  20111  prdsmulrngcl  20147  prdsrngd  20148  prdsringd  20291  prdscrngd  20292  prds1  20293  pwspjmhmmgpd  20298  pwsgprod  20300  rnghmf1o  20423  rhmf1o  20461  rhmimasubrnglem  20533  rnrhmsubrg  20573  rrgsupp  20669  imadrhmcl  20765  isabvd  20780  lmodfopnelem1  20884  lcomfsupp  20888  prdsvscacl  20954  prdslmodd  20955  lmhmco  21030  lmhmplusg  21031  lmhmvsca  21032  lmhmf1o  21033  lmhmeql  21042  lspextmo  21043  rhmpreimaidl  21267  pjfo  21705  dsmmbas2  21727  dsmm0cl  21730  dsmmacl  21731  dsmmsubg  21733  dsmmlss  21734  frlmvplusgvalc  21757  frlmvscaval  21758  frlmplusgvalb  21759  frlmvscavalb  21760  frlmsslss2  21765  frlmphllem  21770  frlmphl  21771  frlmssuvc2  21785  frlmsslsp  21786  frlmup1  21788  frlmup2  21789  frlmup3  21790  frlmup4  21791  islindf4  21828  psrbagfsupp  21909  psrbaglesupp  21912  psrbaglecl  21913  psrbagaddcl  21914  psrbagcon  21915  psrbaglefi  21916  psrbagleadd1  21918  psrbagconf1o  21919  gsumbagdiaglem  21920  psrass1lem  21922  psrvscaval  21939  psrlidm  21950  psrridm  21951  psrass1  21952  psrdi  21953  psrdir  21954  psrascl  21967  mvrf2  21981  mplsubglem  21987  mplvscaval  22004  subrgmvrf  22022  mplbas2  22030  mplind  22058  psrbagev1  22065  psrbagev2  22066  evlslem3  22068  evlslem1  22070  evlsvvval  22081  evlsvar  22083  evladdval  22091  evlmulval  22092  mpfind  22103  ismhp3  22118  mhpmulcl  22125  psdmplcl  22138  psdadd  22139  psdvsca  22140  psdmul  22142  psdmvr  22145  psrplusgpropd  22209  coe1add  22239  coe1addfv  22240  evl1addd  22316  evl1subd  22317  evl1muld  22318  pf1mpf  22327  pf1ind  22330  evls1fpws  22344  ressply1evl  22345  rhmply1vsca  22363  mamudir  22379  mamulid  22416  mamurid  22417  mdetrlin  22577  mdetrsca  22578  mdetralt  22583  mdetunilem7  22593  mdetunilem9  22595  madurid  22619  cnrest2  23261  lmss  23273  lmcnp  23279  cnt0  23321  cnt1  23325  cnhaus  23329  rncmp  23371  conncn  23401  2ndcomap  23433  1stccnp  23437  comppfsc  23507  1stckgenlem  23528  ptbasfi  23556  ptopn  23558  ptclsg  23590  ptcnp  23597  upxp  23598  txtube  23615  txcmplem1  23616  hauseqlcld  23621  xkohaus  23628  xkoptsub  23629  cnmpt11  23638  cnmpt21  23646  cnmpt22f  23650  cnmptcom  23653  qtopss  23690  qtopeu  23691  qtopomap  23693  qtopcmap  23694  kqffn  23700  hmeof1o2  23738  xkocnv  23789  rnelfm  23928  ptcmplem1  24027  cnextfres1  24043  ghmcnp  24090  tgphaus  24092  prdstmdd  24099  prdstgpd  24100  fmucnd  24266  psmetxrge0  24288  isxmet2d  24302  prdsmet  24345  blelrnps  24391  blelrn  24392  xmetresbl  24412  comet  24488  stdbdxmet  24490  met2ndci  24497  prdsxmslem2  24504  isngp3  24573  nmotri  24714  metdsre  24829  bndth  24935  evth  24936  fmcfil  25249  bcthlem4  25304  rrxcph  25369  rrxds  25370  rrxmet  25385  evthicc2  25437  ovolfsf  25448  ovolmge0  25454  ovollb2lem  25465  ovolunlem1a  25473  ovoliunlem1  25479  ovoliun  25482  ovoliun2  25483  ovolscalem1  25490  ovolicc1  25493  ovolicc2lem4  25497  ovolicc2  25499  voliunlem1  25527  voliunlem3  25529  volsup  25533  ioombl1lem2  25536  ioombl1lem4  25538  uniiccdif  25555  uniioombllem2  25560  uniioombllem3  25562  uniioombllem6  25565  volsup2  25582  vitalilem4  25588  mbfeqalem1  25618  mbfmulc2lem  25624  mbfmax  25626  mbfaddlem  25637  mbfadd  25638  mbfsub  25639  mbfsup  25641  mbfinf  25642  itg1ge0  25663  itg1addlem1  25669  i1faddlem  25670  i1fmullem  25671  i1fadd  25672  i1fmul  25673  itg1addlem4  25676  i1fmulclem  25679  i1fmulc  25680  itg1mulc  25681  i1fres  25682  itg10a  25687  itg1ge0a  25688  itg1lea  25689  mbfi1fseqlem3  25694  mbfi1fseqlem4  25695  mbfi1flimlem  25699  mbfmullem2  25701  mbfmul  25703  itg20  25714  itg2lea  25721  itg2splitlem  25725  itg2split  25726  itg2monolem1  25727  itg2monolem2  25728  itg2monolem3  25729  itg2mono  25730  itg2i1fseqle  25731  itg2i1fseq  25732  itg2addlem  25735  itg2gt0  25737  itg2cnlem1  25738  itg2cnlem2  25739  itg2cn  25740  itgitg1  25786  bddmulibl  25816  bddibl  25817  dvidlem  25892  dvaddbr  25915  dvmulbr  25916  dvaddf  25919  dvcmulf  25922  dvrec  25932  dvcnvlem  25953  rolle  25967  dveq0  25977  dv11cn  25978  dvivthlem2  25986  dvivth  25987  dvne0  25988  lhop1lem  25990  lhop1  25991  lhop2  25992  lhop  25993  ftc1cn  26020  tdeglem1  26033  tdeglem3  26034  tdeglem4  26035  mdegleb  26039  mdegldg  26041  mdegaddle  26049  ply1remlem  26140  ply1rem  26141  fta1glem1  26143  fta1glem2  26144  fta1blem  26146  idomrootle  26148  plyeq0lem  26185  plyeq0  26186  plyaddlem1  26188  coeeulem  26199  coeaddlem  26224  coemulc  26230  dgradd2  26243  dgrcolem2  26249  ofmulrt  26258  plyrem  26282  vieta1lem1  26287  vieta1  26289  plyexmo  26290  elqaalem3  26298  aannenlem1  26305  aalioulem2  26310  ulmuni  26370  ulmdvlem1  26378  ulmdv  26381  mbfulm  26384  iblulm  26385  itgulm  26386  rlimcnp2  26943  jensen  26966  amgm  26968  basellem3  27060  basellem7  27064  basellem9  27066  dchrelbas2  27214  dchrmulcl  27226  dchrfi  27232  dchreq  27235  dchrresb  27236  dchrinv  27238  dchr1re  27240  sumdchr2  27247  dchr2sum  27250  lgsqrlem2  27324  lgsqrlem3  27325  rpvmasum2  27489  dchrisum0re  27490  mirf1o  28751  lmif1o  28877  eqeefv  28986  axlowdimlem14  29038  vtxdgfisf  29560  2pthon3v  30026  nvinvfval  30726  sspg  30814  ssps  30816  sspmlem  30818  sspn  30822  lnon0  30884  ubthlem1  30956  pjfn  31795  kbpj  32042  kbass2  32203  elpjrn  32276  ofrn2  32728  off2  32729  ofresid  32730  xppreima2  32739  ofpreima2  32754  suppovss  32769  resf1o  32818  prodindf  32937  indpreima  32940  swrdrn3  33030  pwrssmgc  33075  mgcf1o  33078  gsumfs2d  33137  gsumhashmul  33143  symgcom2  33160  pmtrcnel  33165  pmtrcnel2  33166  pmtrcnelor  33167  cycpmfvlem  33188  cycpmfv3  33191  cycpmcl  33192  cycpmco2rn  33201  cycpmco2  33209  cycpm3cl2  33212  cyc3co2  33216  cyc3evpm  33226  elrgspnlem1  33318  elrgspnlem2  33319  elrgspnlem4  33321  elrgspnsubrunlem1  33323  elrgspnsubrunlem2  33324  gsumind  33420  islinds5  33442  ellspds  33443  elrspunidl  33503  elrspunsn  33504  rhmimaidl  33507  rhmpreimaprmidl  33526  rprmdvdsprod  33609  1arithidomlem2  33611  evls1fn  33635  ply1dg1rt  33655  ply1mulrtss  33657  ply1degltel  33669  ply1degleel  33670  ply1degltlss  33671  ply1gsumz  33674  ig1pmindeg  33677  r1pquslmic  33686  extvfvcl  33695  mplmulmvr  33698  evlextv  33701  mplvrpmmhm  33705  mplvrpmrhm  33706  psrmonprod  33711  esplyfval0  33723  esplyfval2  33724  esplyfv1  33728  esplyfv  33729  esplyfval3  33731  esplyfvaln  33733  esplyind  33734  vieta  33739  exsslsb  33756  ply1degltdimlem  33782  ply1degltdim  33783  dimkerim  33787  fedgmullem2  33790  fedgmul  33791  lvecendof1f1o  33793  fldextrspunlsplem  33833  fldextrspunlsp  33834  irngss  33847  irngnzply1  33851  extdgfialglem2  33853  irngnminplynz  33872  2sqr3minply  33940  cos9thpiminply  33948  cmpcref  34010  rhmpreimacnlem  34044  fsumcvg4  34110  pl1cn  34115  qqhval2lem  34141  esumcvg  34246  ofcf  34263  ofcof  34267  measfn  34364  meascnbl  34379  sibfof  34500  sitgaddlemb  34508  subiwrdlen  34546  rrvfn  34605  plymul02  34706  signsplypnf  34710  signsply0  34711  reprsuc  34775  reprdifc  34787  breprexplema  34790  circlemethhgt  34803  hgt750lemb  34816  f1resrcmplf1dlem  35245  pthhashvtx  35326  cvmopnlem  35476  cvmliftmolem1  35479  cvmliftlem10  35492  cvmlift2lem9a  35501  cvmlift2lem6  35506  cvmlift2lem12  35512  cvmliftphtlem  35515  cvmlift3lem9  35525  mrsubrn  35711  elmrsubrn  35718  elmsubrn  35726  msubrn  35727  mclsind  35768  mclsppslem  35781  mclspps  35782  iprodefisumlem  35938  weiunfrlem  36662  mh-inf3f1  36739  matunitlindflem1  37951  poimirlem1  37956  poimirlem2  37957  poimirlem3  37958  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  poimirlem22  37977  poimirlem23  37978  poimirlem29  37984  poimirlem30  37985  poimirlem31  37986  poimir  37988  mblfinlem2  37993  itg2addnclem3  38008  itg2addnc  38009  itg2gt0cn  38010  ftc1cnnc  38027  ftc1anclem5  38032  ftc1anclem7  38034  ftc1anc  38036  sdclem2  38077  istotbnd3  38106  sstotbnd2  38109  isbnd3  38119  heibor1lem  38144  rrnmet  38164  grpokerinj  38228  isdrngo2  38293  lfl1  39530  lfladdcl  39531  lflvscl  39537  lkr0f  39554  lkrsc  39557  eqlkr2  39560  eqlkr3  39561  ldualvaddval  39591  ldualvsval  39598  tendoeq1  41224  zndvdchrrhm  42426  hashscontpow  42575  aks6d1c3  42576  aks6d1c2lem4  42580  aks6d1c2  42583  sticksstones1  42599  sticksstones2  42600  sticksstones3  42601  sticksstones12a  42610  sticksstones12  42611  aks6d1c6lem2  42624  aks6d1c6lem3  42625  aks6d1c6isolem1  42627  aks6d1c6isolem3  42629  aks6d1c6lem5  42630  aks6d1c7lem1  42633  unitscyglem1  42648  dvun  42805  frlmvscadiccat  42965  fiabv  42995  frlmsnic  42999  mplmapghm  43011  evlsaddval  43018  evlsmulval  43019  selvvvval  43032  evlselvlem  43033  evlselv  43034  fsuppssind  43040  mhphf  43044  ismrcd1  43144  ismrcd2  43145  istopclsd  43146  isnacs3  43156  mzpaddmpt  43187  mzpmulmpt  43188  mzpsubst  43194  mzpcong  43418  fnwe2lem2  43497  islmodfg  43515  kercvrlsm  43529  dgrsub2  43581  mpaaeu  43596  rngunsnply  43615  hausgraph  43651  ofoafg  43800  ofoafo  43802  ofoaid1  43804  ofoaid2  43805  naddcnff  43808  naddcnffn  43809  naddcnffo  43810  naddcnfcom  43812  naddcnfid1  43813  naddcnfass  43815  fsovf1od  44461  brcoffn  44475  clsneiel1  44553  wfximgfd  44608  extoimad  44609  mnringmulrcld  44673  mnurndlem1  44726  caofcan  44768  ofmul12  44770  ofdivrec  44771  ofdivcan4  44772  ofdivdiv2  44773  dvconstbi  44779  binomcxplemnotnn0  44801  relpmin  45397  refsum2cnlem1  45486  ssmapsn  45663  preimaiocmnf  46008  fsumsupp0  46026  fsumsermpt  46027  climinf  46054  climinf2lem  46152  limsupmnflem  46166  limsupvaluz2  46184  supcnvlimsup  46186  limsupgtlem  46223  liminfvalxr  46229  liminflelimsupuz  46231  xlimconst2  46281  climxlim2  46292  icccncfext  46333  dvnprodlem1  46392  volicoff  46441  voliooicof  46442  fourierdlem25  46578  etransclem2  46682  etransclem35  46715  fge0iccico  46816  sge0tsms  46826  sge0sup  46837  sge0resrn  46850  sge0le  46853  sge0fodjrnlem  46862  sge0isum  46873  sge0seq  46892  nnfoctbdjlem  46901  meadjiunlem  46911  omeiunle  46963  hoicvr  46994  ovolval4lem1  47095  ovolval5lem3  47100  ovnovollem1  47102  ovnovollem2  47103  iinhoiicclem  47119  iunhoiioolem  47121  preimaicomnf  47157  smfresal  47234  smfsuplem1  47257  smflimsuplem2  47267  fcoreslem3  47525  fcoreslem4  47526  fcores  47527  isubgredg  48354  upgrimpths  48397  ackvalsucsucval  49176  funchomf  49584  imasubc  49638  imassc  49640  imaid  49641  prcofdiag1  49880  prcofdiag  49881  oppfdiag1  49901  oppfdiag  49903  amgmwlem  50289