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 17	1 ⊢ (𝜑 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 6528  ⟶wf 6529

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 206  df-an 396  df-f 6537

This theorem is referenced by:  fnconstg  6769  f1fn  6778  fofn  6797  f1ofn  6824  feqmptd  6950  fprb  7187  cocan1  7281  oprres  7568  off  7681  ofco  7686  caofref  7692  caofid0l  7694  caofid0r  7695  caofid1  7696  caofid2  7697  caofrss  7699  caoftrn  7701  fo2ndf  8101  fnwelem  8111  fnse  8113  suppsnop  8157  suppss  8173  suppssOLD  8174  suppssr  8175  suppssrg  8176  suppssof1  8179  suppofssd  8183  suppofss1d  8184  suppofss2d  8185  suppcoss  8187  smocdmdom  8363  elmapfn  8855  ralxpmap  8886  omxpenlem  9069  mapen  9137  f1finf1o  9267  f1finf1oOLD  9268  unirnffid  9340  fdmfifsupp  9369  mapfien  9399  intrnfi  9407  marypha2  9430  ordtypelem7  9515  wemapsolem  9541  wemapso  9542  wemapso2lem  9543  unxpwdom2  9579  ixpiunwdom  9581  cantnfle  9662  cantnfp1lem2  9670  cantnfp1lem3  9671  cantnfp1  9672  oemapvali  9675  cantnflem1a  9676  cantnflem1c  9678  cantnflem3  9682  cantnf  9684  cnfcomlem  9690  cnfcom3  9695  updjudhcoinlf  9923  updjudhcoinrg  9924  fseqenlem1  10015  numacn  10040  infpwfien  10053  isf32lem2  10345  isf34lem7  10370  isf34lem6  10371  unirnfdomd  10558  ofsubeq0  12206  ofnegsub  12207  ofsubge0  12208  seqf1olem2  14005  resunimafz0  14401  wrdfn  14475  swrdvalfn  14598  pfxfn  14628  pfxid  14631  cats1un  14668  cshwfn  14748  ccatco  14783  limsupgle  15418  o1of2  15554  o1rlimmul  15560  isercolllem2  15609  isercoll  15611  isercoll2  15612  climsup  15613  fsumss  15668  ruclem11  16180  vdwlem2  16914  vdwlem6  16918  vdwlem9  16921  vdwlem12  16924  0ram  16952  ramub1lem1  16958  pwsle  17437  pwsleval  17438  pwsvscaval  17440  mrcuni  17564  mrcun  17565  invf1o  17715  funcres2c  17853  setcmon  18039  setcepi  18040  uncfcurf  18194  yoniso  18240  isacs4lem  18499  acsmapd  18509  gsumval2  18609  mgmhmf1o  18623  resmgmhm2b  18636  mgmhmima  18638  mgmhmeql  18639  prdsplusgsgrpcl  18655  prdssgrpd  18656  prdsplusgcl  18688  prdsidlem  18689  prdsmndd  18690  mhmf1o  18716  resmhm2b  18737  mhmimalem  18739  mhmima  18740  mhmeql  18741  prdspjmhm  18744  pwsco1mhm  18747  pwsco2mhm  18748  gsumwmhm  18760  frmdss2  18778  grpinvf1o  18928  prdsinvlem  18967  cycsubgcl  19122  ghmrn  19144  ghmpreima  19153  ghmeql  19154  ghmnsgima  19155  ghmnsgpreima  19156  ghmeqker  19158  ghmf1o  19163  gass  19207  cntzmhm  19247  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  prdsmulrngcl  20070  prdsrngd  20071  prdsringd  20210  prdscrngd  20211  prds1  20212  pwspjmhmmgpd  20217  rnghmf1o  20344  rhmf1o  20383  rhmimasubrnglem  20455  rnrhmsubrg  20497  imadrhmcl  20638  isabvd  20653  lmodfopnelem1  20734  lcomfsupp  20738  prdsvscacl  20805  prdslmodd  20806  lmhmco  20881  lmhmplusg  20882  lmhmvsca  20883  lmhmf1o  20884  lmhmeql  20893  lspextmo  20894  rrgsupp  21191  pjfo  21578  dsmmbas2  21600  dsmm0cl  21603  dsmmacl  21604  dsmmsubg  21606  dsmmlss  21607  frlmvplusgvalc  21630  frlmvscaval  21631  frlmplusgvalb  21632  frlmvscavalb  21633  frlmsslss2  21638  frlmphllem  21643  frlmphl  21644  frlmssuvc2  21658  frlmsslsp  21659  frlmup1  21661  frlmup2  21662  frlmup3  21663  frlmup4  21664  islindf4  21701  psrbagfsupp  21782  psrbaglesupp  21786  psrbaglesuppOLD  21787  psrbaglecl  21788  psrbagaddcl  21790  psrbagcon  21792  psrbagconOLD  21793  psrbaglefi  21794  psrbaglefiOLD  21795  psrbagconf1o  21798  psrbagconf1oOLD  21799  gsumbagdiaglemOLD  21800  gsumbagdiaglem  21803  psrass1lem  21805  psrvscaval  21821  psrlidm  21833  psrridm  21834  psrass1  21835  psrdi  21836  psrdir  21837  mvrf2  21862  mplsubglem  21868  mplvscaval  21885  subrgmvrf  21899  mplbas2  21907  mplind  21941  psrbagev1  21948  psrbagev1OLD  21949  psrbagev2  21950  evlslem3  21953  evlslem1  21955  evlsvar  21963  mpfind  21980  ismhp3  21994  mhpmulcl  22000  psdmplcl  22013  psdadd  22014  psdvsca  22015  psrplusgpropd  22077  coe1add  22105  coe1addfv  22106  evl1addd  22182  evl1subd  22183  evl1muld  22184  pf1mpf  22193  pf1ind  22196  mamudir  22226  mamulid  22265  mamurid  22266  mdetrlin  22426  mdetrsca  22427  mdetralt  22432  mdetunilem7  22442  mdetunilem9  22444  madurid  22468  cnrest2  23112  lmss  23124  lmcnp  23130  cnt0  23172  cnt1  23176  cnhaus  23180  rncmp  23222  conncn  23252  2ndcomap  23284  1stccnp  23288  comppfsc  23358  1stckgenlem  23379  ptbasfi  23407  ptopn  23409  ptclsg  23441  ptcnp  23448  upxp  23449  txtube  23466  txcmplem1  23467  hauseqlcld  23472  xkohaus  23479  xkoptsub  23480  cnmpt11  23489  cnmpt21  23497  cnmpt22f  23501  cnmptcom  23504  qtopss  23541  qtopeu  23542  qtopomap  23544  qtopcmap  23545  kqffn  23551  hmeof1o2  23589  xkocnv  23640  rnelfm  23779  ptcmplem1  23878  cnextfres1  23894  ghmcnp  23941  tgphaus  23943  prdstmdd  23950  prdstgpd  23951  fmucnd  24119  psmetxrge0  24141  isxmet2d  24155  prdsmet  24198  blelrnps  24244  blelrn  24245  xmetresbl  24265  comet  24344  stdbdxmet  24346  met2ndci  24353  prdsxmslem2  24360  isngp3  24429  nmotri  24578  metdsre  24691  bndth  24806  evth  24807  fmcfil  25122  bcthlem4  25177  rrxcph  25242  rrxds  25243  rrxmet  25258  evthicc2  25311  ovolfsf  25322  ovolmge0  25328  ovollb2lem  25339  ovolunlem1a  25347  ovoliunlem1  25353  ovoliun  25356  ovoliun2  25357  ovolscalem1  25364  ovolicc1  25367  ovolicc2lem4  25371  ovolicc2  25373  voliunlem1  25401  voliunlem3  25403  volsup  25407  ioombl1lem2  25410  ioombl1lem4  25412  uniiccdif  25429  uniioombllem2  25434  uniioombllem3  25436  uniioombllem6  25439  volsup2  25456  vitalilem4  25462  mbfeqalem1  25492  mbfmulc2lem  25498  mbfmax  25500  mbfaddlem  25511  mbfadd  25512  mbfsub  25513  mbfsup  25515  mbfinf  25516  itg1ge0  25537  itg1addlem1  25543  i1faddlem  25544  i1fmullem  25545  i1fadd  25546  i1fmul  25547  itg1addlem4  25550  itg1addlem4OLD  25551  i1fmulclem  25554  i1fmulc  25555  itg1mulc  25556  i1fres  25557  itg10a  25562  itg1ge0a  25563  itg1lea  25564  mbfi1fseqlem3  25569  mbfi1fseqlem4  25570  mbfi1flimlem  25574  mbfmullem2  25576  mbfmul  25578  itg20  25589  itg2lea  25596  itg2splitlem  25600  itg2split  25601  itg2monolem1  25602  itg2monolem2  25603  itg2monolem3  25604  itg2mono  25605  itg2i1fseqle  25606  itg2i1fseq  25607  itg2addlem  25610  itg2gt0  25612  itg2cnlem1  25613  itg2cnlem2  25614  itg2cn  25615  itgitg1  25660  bddmulibl  25690  bddibl  25691  dvidlem  25766  dvaddbr  25790  dvmulbr  25791  dvmulbrOLD  25792  dvaddf  25795  dvcmulf  25798  dvrec  25809  dvcnvlem  25830  rolle  25844  dveq0  25855  dv11cn  25856  dvivthlem2  25864  dvivth  25865  dvne0  25866  lhop1lem  25868  lhop1  25869  lhop2  25870  lhop  25871  ftc1cn  25900  tdeglem1  25913  tdeglem3  25915  tdeglem4  25917  tdeglem4OLD  25918  mdegleb  25922  mdegldg  25924  mdegaddle  25932  ply1remlem  26020  ply1rem  26021  fta1glem1  26023  fta1glem2  26024  fta1blem  26026  plyeq0lem  26064  plyeq0  26065  plyaddlem1  26067  coeeulem  26078  coeaddlem  26103  coemulc  26109  dgradd2  26123  dgrcolem2  26129  ofmulrt  26136  plyrem  26159  vieta1lem1  26164  vieta1  26166  plyexmo  26167  elqaalem3  26175  aannenlem1  26182  aalioulem2  26187  ulmuni  26245  ulmdvlem1  26253  ulmdv  26256  mbfulm  26259  iblulm  26260  itgulm  26261  rlimcnp2  26814  jensen  26837  amgm  26839  basellem3  26931  basellem7  26935  basellem9  26937  dchrelbas2  27086  dchrmulcl  27098  dchrfi  27104  dchreq  27107  dchrresb  27108  dchrinv  27110  dchr1re  27112  sumdchr2  27119  dchr2sum  27122  lgsqrlem2  27196  lgsqrlem3  27197  rpvmasum2  27361  dchrisum0re  27362  mirf1o  28389  lmif1o  28515  eqeefv  28630  axlowdimlem14  28682  vtxdgfisf  29202  2pthon3v  29666  nvinvfval  30362  sspg  30450  ssps  30452  sspmlem  30454  sspn  30458  lnon0  30520  ubthlem1  30592  pjfn  31431  kbpj  31678  kbass2  31839  elpjrn  31912  ofrn2  32334  off2  32335  ofresid  32336  xppreima2  32345  ofpreima2  32360  suppovss  32375  resf1o  32424  swrdrn3  32586  pwrssmgc  32637  mgcf1o  32640  gsumhashmul  32676  gsumle  32710  symgcom2  32713  pmtrcnel  32718  pmtrcnel2  32719  pmtrcnelor  32720  cycpmfvlem  32739  cycpmfv3  32742  cycpmcl  32743  cycpmco2rn  32752  cycpmco2  32760  cycpm3cl2  32763  cyc3co2  32767  cyc3evpm  32777  islinds5  32949  ellspds  32950  ghmquskerlem1  32997  ghmquskerco  32998  ghmquskerlem3  33000  ghmqusker  33001  rhmpreimaidl  33006  elrspunidl  33015  elrspunsn  33016  rhmimaidl  33019  rhmpreimaprmidl  33039  evls1fn  33107  evls1fpws  33113  ressply1evl  33114  ply1degltel  33131  ply1degleel  33132  ply1degltlss  33133  ply1gsumz  33135  ig1pmindeg  33138  r1pquslmic  33147  ply1degltdimlem  33186  ply1degltdim  33187  dimkerim  33191  fedgmullem2  33194  fedgmul  33195  irngss  33231  irngnzply1  33235  irngnminplynz  33251  cmpcref  33319  rhmpreimacnlem  33353  fsumcvg4  33419  pl1cn  33424  qqhval2lem  33450  prodindf  33510  indpreima  33512  esumcvg  33573  ofcf  33590  ofcof  33594  measfn  33691  meascnbl  33706  sibfof  33828  sitgaddlemb  33836  subiwrdlen  33874  rrvfn  33933  plymul02  34046  signsplypnf  34050  signsply0  34051  reprsuc  34116  reprdifc  34128  breprexplema  34131  circlemethhgt  34144  hgt750lemb  34157  f1resrcmplf1dlem  34578  pthhashvtx  34607  cvmopnlem  34758  cvmliftmolem1  34761  cvmliftlem10  34774  cvmlift2lem9a  34783  cvmlift2lem6  34788  cvmlift2lem12  34794  cvmliftphtlem  34797  cvmlift3lem9  34807  mrsubrn  34993  elmrsubrn  35000  elmsubrn  35008  msubrn  35009  mclsind  35050  mclsppslem  35063  mclspps  35064  iprodefisumlem  35205  matunitlindflem1  36974  poimirlem1  36979  poimirlem2  36980  poimirlem3  36981  poimirlem16  36994  poimirlem17  36995  poimirlem19  36997  poimirlem20  36998  poimirlem22  37000  poimirlem23  37001  poimirlem29  37007  poimirlem30  37008  poimirlem31  37009  poimir  37011  mblfinlem2  37016  itg2addnclem3  37031  itg2addnc  37032  itg2gt0cn  37033  ftc1cnnc  37050  ftc1anclem5  37055  ftc1anclem7  37057  ftc1anc  37059  sdclem2  37100  istotbnd3  37129  sstotbnd2  37132  isbnd3  37142  heibor1lem  37167  rrnmet  37187  grpokerinj  37251  isdrngo2  37316  lfl1  38430  lfladdcl  38431  lflvscl  38437  lkr0f  38454  lkrsc  38457  eqlkr2  38460  eqlkr3  38461  ldualvaddval  38491  ldualvsval  38498  tendoeq1  40125  sticksstones1  41455  sticksstones2  41456  sticksstones3  41457  sticksstones12a  41466  sticksstones12  41467  metakunt19  41496  metakunt25  41502  metakunt33  41510  frlmvscadiccat  41573  frlmsnic  41599  pwsgprod  41603  mplmapghm  41617  evlsvvval  41624  evlsaddval  41629  evlsmulval  41630  evladdval  41636  evlmulval  41637  selvvvval  41646  evlselvlem  41647  evlselv  41648  fsuppssind  41654  mhphf  41658  ismrcd1  41925  ismrcd2  41926  istopclsd  41927  isnacs3  41937  mzpaddmpt  41968  mzpmulmpt  41969  mzpsubst  41975  mzpcong  42200  fnwe2lem2  42282  islmodfg  42300  kercvrlsm  42314  dgrsub2  42366  mpaaeu  42381  rngunsnply  42404  idomrootle  42426  hausgraph  42443  ofoafg  42593  ofoafo  42595  ofoaid1  42597  ofoaid2  42598  naddcnff  42601  naddcnffn  42602  naddcnffo  42603  naddcnfcom  42605  naddcnfid1  42606  naddcnfass  42608  fsovf1od  43256  brcoffn  43270  clsneiel1  43348  wfximgfd  43404  extoimad  43405  mnringmulrcld  43476  mnurndlem1  43529  caofcan  43571  ofmul12  43573  ofdivrec  43574  ofdivcan4  43575  ofdivdiv2  43576  dvconstbi  43582  binomcxplemnotnn0  43604  refsum2cnlem1  44210  ssmapsn  44400  preimaiocmnf  44759  fsumsupp0  44779  fsumsermpt  44780  climinf  44807  climinf2lem  44907  limsupmnflem  44921  limsupvaluz2  44939  supcnvlimsup  44941  limsupgtlem  44978  liminfvalxr  44984  liminflelimsupuz  44986  xlimconst2  45036  climxlim2  45047  icccncfext  45088  dvnprodlem1  45147  volicoff  45196  voliooicof  45197  fourierdlem25  45333  etransclem2  45437  etransclem35  45470  fge0iccico  45571  sge0tsms  45581  sge0sup  45592  sge0resrn  45605  sge0le  45608  sge0fodjrnlem  45617  sge0isum  45628  sge0seq  45647  nnfoctbdjlem  45656  meadjiunlem  45666  omeiunle  45718  hoicvr  45749  ovolval4lem1  45850  ovolval5lem3  45855  ovnovollem1  45857  ovnovollem2  45858  iinhoiicclem  45874  iunhoiioolem  45876  preimaicomnf  45912  smfresal  45989  smfsuplem1  46012  smflimsuplem2  46022  fcoreslem3  46260  fcoreslem4  46261  fcores  46262  ackvalsucsucval  47562  amgmwlem  48037