Theorem ffnd 6708

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

Syntax hints:   → wi 4   Fn wfn 6533  ⟶wf 6534

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 210  df-an 401  df-f 6542

This theorem is referenced by:  fnconstg  6768  f1fn  6777  fofn  6796  f1ofn  6823  feqmptd  6951  fssrescdmd  7124  fprb  7194  cocan1  7291  oprres  7580  off  7694  coof  7700  ofco  7701  caofref  7707  caofid0l  7709  caofid0r  7710  caofid1  7711  caofid2  7712  caofrss  7715  caoftrn  7717  fo2ndf  8117  fnwelem  8128  fnse  8130  suppsnop  8175  suppss  8191  suppssr  8192  suppssrg  8193  suppssof1  8196  suppofssd  8200  suppofss1d  8201  suppofss2d  8202  suppcoss  8204  smocdmdom  8356  elmapfn  8863  ralxpmap  8895  omxpenlem  9067  mapen  9130  f1finf1o  9234  unirnffid  9305  fdmfifsupp  9336  mapfien  9369  intrnfi  9377  marypha2  9400  ordtypelem7  9487  wemapsolem  9513  wemapso  9514  wemapso2lem  9515  unxpwdom2  9551  ixpiunwdom  9553  cantnfle  9641  cantnfp1lem2  9649  cantnfp1lem3  9650  cantnfp1  9651  oemapvali  9654  cantnflem1a  9655  cantnflem1c  9657  cantnflem3  9661  cantnf  9663  cnfcomlem  9669  cnfcom3  9674  updjudhcoinlf  9919  updjudhcoinrg  9920  fseqenlem1  10009  numacn  10034  infpwfien  10047  isf32lem2  10339  isf34lem7  10364  isf34lem6  10365  unirnfdomd  10553  ofsubeq0  12216  ofnegsub  12217  ofsubge0  12218  seqf1olem2  14080  resunimafz0  14484  wrdfn  14567  swrdvalfn  14691  pfxfn  14721  pfxid  14724  cats1un  14760  cshwfn  14840  ccatco  14874  limsupgle  15530  o1of2  15666  o1rlimmul  15672  isercolllem2  15719  isercoll  15721  isercoll2  15722  climsup  15723  fsumss  15778  ruclem11  16297  vdwlem2  17043  vdwlem6  17047  vdwlem9  17050  vdwlem12  17053  0ram  17081  ramub1lem1  17087  pwsle  17547  pwsleval  17548  pwsvscaval  17550  mrcuni  17678  mrcun  17679  invf1o  17827  funcres2c  17961  setcmon  18145  setcepi  18146  uncfcurf  18296  yoniso  18342  isacs4lem  18601  acsmapd  18611  chnso  18681  gsumval2  18745  mgmhmf1o  18759  resmgmhm2b  18772  mgmhmima  18774  mgmhmeql  18775  prdsplusgsgrpcl  18791  prdssgrpd  18792  prdsplusgcl  18827  prdsidlem  18828  prdsmndd  18829  mhmf1o  18855  resmhm2b  18882  mhmimalem  18884  mhmima  18885  mhmeql  18886  prdspjmhm  18889  pwsco1mhm  18892  pwsco2mhm  18893  gsumwmhm  18905  frmdss2  18923  grpinvf1o  19076  prdsinvlem  19116  cycsubgcl  19278  ghmrn  19300  ghmpreima  19309  ghmeql  19310  ghmnsgima  19311  ghmnsgpreima  19312  ghmeqker  19314  ghmf1o  19319  ghmqusnsglem1  19351  ghmqusnsg  19353  ghmquskerlem1  19354  ghmquskerco  19355  ghmquskerlem3  19357  ghmqusker  19358  gass  19372  cntzmhm  19412  symgextres  19496  gsmsymgrfixlem1  19498  fvcosymgeq  19500  f1omvdconj  19517  pmtrfinv  19532  symgtrinv  19543  pmtr3ncomlem1  19544  sygbasnfpfi  19583  efginvrel2  19798  efgredleme  19814  ghmplusg  19917  prdscmnd  19932  gsumval3a  19974  gsumval3eu  19975  gsumzaddlem  19992  gsumzsplit  19998  gsumpt  20033  prdsgsum  20052  dprdfcntz  20088  dprdfadd  20093  dprdfeq0  20095  dprdf11  20096  dprdlub  20099  dprdspan  20100  dprd2dlem1  20114  dmdprdpr  20122  dprdpr  20123  dpjlem  20124  ablfac1eu  20146  gsumle  20216  prdsmulrngcl  20254  prdsrngd  20255  prdsringd  20403  prdscrngd  20404  prds1  20405  pwspjmhmmgpd  20410  pwsgprod  20412  rnghmf1o  20535  rhmf1o  20574  rhmimasubrnglem  20651  rnrhmsubrg  20691  rrgsupp  20787  imadrhmcl  20881  isabvd  20896  lmodfopnelem1  21000  lcomfsupp  21004  prdsvscacl  21070  prdslmodd  21071  lmhmco  21145  lmhmplusg  21146  lmhmvsca  21147  lmhmf1o  21148  lmhmeql  21157  lspextmo  21158  rhmpreimaidl  21397  rhmpreimaprmidl  21460  pjfo  21846  dsmmbas2  21868  dsmm0cl  21871  dsmmacl  21872  dsmmsubg  21874  dsmmlss  21875  frlmvplusgvalc  21898  frlmvscaval  21899  frlmplusgvalb  21900  frlmvscavalb  21901  frlmsslss2  21906  frlmphllem  21911  frlmphl  21912  frlmssuvc2  21926  frlmsslsp  21927  frlmup1  21929  frlmup2  21930  frlmup3  21931  frlmup4  21932  islindf4  21969  psrbagfsupp  22050  psrbaglesupp  22053  psrbaglecl  22054  psrbagaddcl  22055  psrbagcon  22056  psrbaglefi  22057  psrbagleadd1  22059  psrbagconf1o  22060  gsumbagdiaglem  22062  psrass1lem  22064  psrvscaval  22081  psrlidm  22092  psrridm  22093  psrass1  22094  psrdi  22095  psrdir  22096  psrascl  22109  mvrf2  22123  mplsubglem  22129  mplvscaval  22146  subrgmvrf  22166  mplbas2  22174  mplind  22202  psrbagev1  22209  psrbagev2  22210  evlslem3  22212  evlslem1  22214  evlsvvval  22225  evlsvar  22227  evladdval  22235  evlmulval  22236  mpfind  22247  mplmapghm  22254  evlsaddval  22261  evlsmulval  22262  selvvvval  22274  ismhp3  22286  mhpmulcl  22293  psdmplcl  22306  psdadd  22307  psdvsca  22308  psdmul  22310  psdmvr  22313  psrplusgpropd  22376  coe1add  22406  coe1addfv  22407  evl1addd  22482  evl1subd  22483  evl1muld  22484  pf1mpf  22493  pf1ind  22496  evls1fpws  22510  ressply1evl  22511  rhmply1vsca  22526  mamudir  22542  mamulid  22579  mamurid  22580  mdetrlin  22740  mdetrsca  22741  mdetralt  22746  mdetunilem7  22756  mdetunilem9  22758  madurid  22782  cnrest2  23424  lmss  23436  lmcnp  23442  cnt0  23484  cnt1  23488  cnhaus  23492  rncmp  23534  conncn  23564  2ndcomap  23596  1stccnp  23600  comppfsc  23670  1stckgenlem  23691  ptbasfi  23719  ptopn  23721  ptclsg  23753  ptcnp  23760  upxp  23761  txtube  23778  txcmplem1  23779  hauseqlcld  23784  xkohaus  23791  xkoptsub  23792  cnmpt11  23801  cnmpt21  23809  cnmpt22f  23813  cnmptcom  23816  qtopss  23853  qtopeu  23854  qtopomap  23856  qtopcmap  23857  kqffn  23863  hmeof1o2  23901  xkocnv  23952  rnelfm  24091  ptcmplem1  24190  cnextfres1  24206  ghmcnp  24253  tgphaus  24255  prdstmdd  24262  prdstgpd  24263  fmucnd  24429  psmetxrge0  24451  isxmet2d  24465  prdsmet  24508  blelrnps  24554  blelrn  24555  xmetresbl  24575  comet  24651  stdbdxmet  24653  met2ndci  24660  prdsxmslem2  24667  isngp3  24736  nmotri  24877  metdsre  24992  bndth  25098  evth  25099  fmcfil  25412  bcthlem4  25467  rrxcph  25532  rrxds  25533  rrxmet  25548  evthicc2  25600  ovolfsf  25611  ovolmge0  25617  ovollb2lem  25628  ovolunlem1a  25636  ovoliunlem1  25642  ovoliun  25645  ovoliun2  25646  ovolscalem1  25653  ovolicc1  25656  ovolicc2lem4  25660  ovolicc2  25662  voliunlem1  25690  voliunlem3  25692  volsup  25696  ioombl1lem2  25699  ioombl1lem4  25701  uniiccdif  25718  uniioombllem2  25723  uniioombllem3  25725  uniioombllem6  25728  volsup2  25745  vitalilem4  25751  mbfeqalem1  25781  mbfmulc2lem  25787  mbfmax  25789  mbfaddlem  25800  mbfadd  25801  mbfsub  25802  mbfsup  25804  mbfinf  25805  itg1ge0  25826  itg1addlem1  25832  i1faddlem  25833  i1fmullem  25834  i1fadd  25835  i1fmul  25836  itg1addlem4  25839  i1fmulclem  25842  i1fmulc  25843  itg1mulc  25844  i1fres  25845  itg10a  25850  itg1ge0a  25851  itg1lea  25852  mbfi1fseqlem3  25857  mbfi1fseqlem4  25858  mbfi1flimlem  25862  mbfmullem2  25864  mbfmul  25866  itg20  25877  itg2lea  25884  itg2splitlem  25888  itg2split  25889  itg2monolem1  25890  itg2monolem2  25891  itg2monolem3  25892  itg2mono  25893  itg2i1fseqle  25894  itg2i1fseq  25895  itg2addlem  25898  itg2gt0  25900  itg2cnlem1  25901  itg2cnlem2  25902  itg2cn  25903  itgitg1  25949  bddmulibl  25979  bddibl  25980  dvidlem  26055  dvaddbr  26078  dvmulbr  26079  dvaddf  26082  dvcmulf  26085  dvrec  26095  dvcnvlem  26116  rolle  26130  dveq0  26140  dv11cn  26141  dvivthlem2  26149  dvivth  26150  dvne0  26151  lhop1lem  26153  lhop1  26154  lhop2  26155  lhop  26156  ftc1cn  26183  tdeglem1  26196  tdeglem3  26197  tdeglem4  26198  mdegleb  26202  mdegldg  26204  mdegaddle  26212  ply1remlem  26303  ply1rem  26304  fta1glem1  26306  fta1glem2  26307  fta1blem  26309  idomrootle  26311  plyeq0lem  26348  plyeq0  26349  plyaddlem1  26351  coeeulem  26362  coeaddlem  26387  coemulc  26393  dgradd2  26406  dgrcolem2  26412  ofmulrt  26421  plymul02  26422  plyrem  26447  vieta1lem1  26452  vieta1  26454  plyexmo  26455  elqaalem3  26463  aannenlem1  26472  aalioulem2  26477  ulmuni  26536  ulmdvlem1  26544  ulmdv  26547  mbfulm  26550  iblulm  26551  itgulm  26552  rlimcnp2  27112  jensen  27134  amgm  27136  basellem3  27228  basellem7  27232  basellem9  27234  dchrelbas2  27382  dchrmulcl  27394  dchrfi  27400  dchreq  27403  dchrresb  27404  dchrinv  27406  dchr1re  27408  sumdchr2  27415  dchr2sum  27418  lgsqrlem2  27492  lgsqrlem3  27493  rpvmasum2  27657  dchrisum0re  27658  mirf1o  28927  lmif1o  29085  eqeefv  29234  axlowdimlem14  29286  vtxdgfisf  29807  2pthon3v  30273  nvinvfval  30973  sspg  31061  ssps  31063  sspmlem  31065  sspn  31069  lnon0  31131  ubthlem1  31203  pjfn  32042  kbpj  32289  kbass2  32450  elpjrn  32523  ofrn2  32966  off2  32967  ofresid  32968  xppreima2  32977  ofpreima2  32992  suppovss  33007  resf1o  33056  prodindf  33163  indpreima  33166  swrdrn3  33256  pwrssmgc  33301  mgcf1o  33304  gsumfs2d  33362  gsumhashmul  33368  symgcom2  33385  pmtrcnel  33390  pmtrcnel2  33391  pmtrcnelor  33392  cycpmfvlem  33413  cycpmfv3  33416  cycpmcl  33417  cycpmco2rn  33426  cycpmco2  33434  cycpm3cl2  33437  cyc3co2  33441  cyc3evpm  33451  elrgspnlem1  33543  elrgspnlem2  33544  elrgspnlem4  33546  elrgspnsubrunlem1  33548  elrgspnsubrunlem2  33549  gsumind  33646  islinds5  33663  ellspds  33664  elrspunidl  33717  elrspunsn  33718  rhmimaidl  33721  rprmdvdsprod  33805  1arithidomlem2  33807  evls1fn  33831  ply1dg1rt  33851  ply1mulrtss  33853  ply1degltel  33865  ply1degleel  33866  ply1degltlss  33867  ply1gsumz  33870  ig1pmindeg  33873  r1pquslmic  33881  0mplrim  33885  mplasclco  33887  selvply1rhmlema  33889  selvply1rhmlemb  33890  selvply1rhmlem1  33891  selvply1rhmlem4  33894  selvply1rhm0  33897  extvfvcl  33907  mplmulmvr  33910  evlextv  33913  mplvrpmmhm  33917  mplvrpmrhm  33918  psrmonprod  33923  esplyfval0  33935  esplyfval2  33936  esplyfv1  33940  esplyfv  33941  esplyfval3  33943  esplyfvaln  33945  esplyind  33946  vieta  33951  exsslsb  33968  ply1degltdimlem  33993  ply1degltdim  33994  dimkerim  33998  fedgmullem2  34001  fedgmul  34002  lvecendof1f1o  34004  fldextrspunlsplem  34044  fldextrspunlsp  34045  irngss  34058  irngnzply1  34062  extdgfialglem2  34064  irngnminplynz  34083  2sqr3minply  34151  cos9thpiminply  34159  cmpcref  34221  rhmpreimacnlem  34255  fsumcvg4  34321  pl1cn  34326  qqhval2lem  34352  esumcvg  34457  ofcf  34474  ofcof  34478  measfn  34575  meascnbl  34590  sibfof  34711  sitgaddlemb  34719  subiwrdlen  34757  rrvfn  34816  signsplypnf  34918  signsply0  34919  reprsuc  34983  reprdifc  34995  breprexplema  34998  circlemethhgt  35011  hgt750lemb  35024  f1resrcmplf1dlem  35455  pthhashvtx  35601  cvmopnlem  35751  cvmliftmolem1  35754  cvmliftlem10  35767  cvmlift2lem9a  35776  cvmlift2lem6  35781  cvmlift2lem12  35787  cvmliftphtlem  35790  cvmlift3lem9  35800  mrsubrn  35986  elmrsubrn  35993  elmsubrn  36001  msubrn  36002  mclsind  36043  mclsppslem  36056  mclspps  36057  iprodefisumlem  36213  weiunfrlem  36956  mh-inf3f1  37033  matunitlindflem1  38248  poimirlem1  38253  poimirlem2  38254  poimirlem3  38255  poimirlem16  38268  poimirlem17  38269  poimirlem19  38271  poimirlem20  38272  poimirlem22  38274  poimirlem23  38275  poimirlem29  38281  poimirlem30  38282  poimirlem31  38283  poimir  38285  mblfinlem2  38290  itg2addnclem3  38305  itg2addnc  38306  itg2gt0cn  38307  ftc1cnnc  38324  ftc1anclem5  38329  ftc1anclem7  38331  ftc1anc  38333  sdclem2  38374  istotbnd3  38403  sstotbnd2  38406  isbnd3  38416  heibor1lem  38441  rrnmet  38461  grpokerinj  38525  isdrngo2  38590  lfl1  39825  lfladdcl  39826  lflvscl  39832  lkr0f  39849  lkrsc  39852  eqlkr2  39855  eqlkr3  39856  ldualvaddval  39886  ldualvsval  39893  tendoeq1  41519  zndvdchrrhm  42721  hashscontpow  42870  aks6d1c3  42871  aks6d1c2lem4  42875  aks6d1c2  42878  sticksstones1  42894  sticksstones2  42895  sticksstones3  42896  sticksstones12a  42905  sticksstones12  42906  aks6d1c6lem2  42919  aks6d1c6lem3  42920  aks6d1c6isolem1  42922  aks6d1c6isolem3  42924  aks6d1c6lem5  42925  aks6d1c7lem1  42928  unitscyglem1  42943  dvun  43101  frlmvscadiccat  43261  fiabv  43287  frlmsnic  43291  evlselvlem  43303  evlselv  43304  fsuppssind  43308  mhphf  43312  ismrcd1  43412  ismrcd2  43413  istopclsd  43414  isnacs3  43424  mzpaddmpt  43455  mzpmulmpt  43456  mzpsubst  43462  mzpcong  43682  fnwe2lem2  43761  islmodfg  43779  kercvrlsm  43793  dgrsub2  43845  mpaaeu  43860  rngunsnply  43879  hausgraph  43915  ofoafg  44064  ofoafo  44066  ofoaid1  44068  ofoaid2  44069  naddcnff  44072  naddcnffn  44073  naddcnffo  44074  naddcnfcom  44076  naddcnfid1  44077  naddcnfass  44079  fsovf1od  44725  brcoffn  44739  clsneiel1  44817  wfximgfd  44872  extoimad  44873  mnringmulrcld  44935  mnurndlem1  44974  caofcan  45016  ofmul12  45018  ofdivrec  45019  ofdivcan4  45020  ofdivdiv2  45021  dvconstbi  45027  binomcxplemnotnn0  45049  relpmin  45644  refsum2cnlem1  45740  ssmapsn  45915  preimaiocmnf  46259  fsumsupp0  46277  fsumsermpt  46278  climinf  46305  climinf2lem  46403  limsupmnflem  46417  limsupvaluz2  46435  supcnvlimsup  46437  limsupgtlem  46474  liminfvalxr  46480  liminflelimsupuz  46482  xlimconst2  46532  climxlim2  46543  icccncfext  46584  dvnprodlem1  46643  volicoff  46692  voliooicof  46693  fourierdlem25  46829  fourierdlem48  46851  fourierdlem49  46852  etransclem2  46933  etransclem35  46966  fge0iccico  47067  sge0tsms  47077  sge0sup  47088  sge0resrn  47101  sge0le  47104  sge0fodjrnlem  47113  sge0isum  47124  sge0seq  47143  nnfoctbdjlem  47152  meadjiunlem  47162  omeiunle  47214  hoicvr  47245  ovolval4lem1  47346  ovolval5lem3  47351  ovnovollem1  47353  ovnovollem2  47354  iinhoiicclem  47370  iunhoiioolem  47372  preimaicomnf  47408  smfresal  47485  smfsuplem1  47508  smflimsuplem2  47518  fcoreslem3  47785  fcoreslem4  47786  fcores  47787  isubgredg  48614  upgrimpths  48657  ackvalsucsucval  49451  funchomf  49858  imasubc  49912  imassc  49914  imaid  49915  prcofdiag1  50154  prcofdiag  50155  oppfdiag1  50175  oppfdiag  50177  amgmwlem  50585