Theorem ffnd 6610

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

Syntax hints:   → wi 4   Fn wfn 6432  ⟶wf 6433

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 397  df-f 6441

This theorem is referenced by:  fnconstg  6671  f1fn  6680  fofn  6699  f1ofn  6726  feqmptd  6846  fprb  7078  rnmptcOLD  7092  cocan1  7172  oprres  7449  off  7560  ofco  7565  caofref  7571  caofid0l  7573  caofid0r  7574  caofid1  7575  caofid2  7576  caofrss  7578  caoftrn  7580  fo2ndf  7971  fnwelem  7981  fnse  7983  suppsnop  8003  suppss  8019  suppssOLD  8020  suppssr  8021  suppssrg  8022  suppssof1  8024  suppofssd  8028  suppofss1d  8029  suppofss2d  8030  suppcoss  8032  smorndom  8208  elmapfn  8662  ralxpmap  8693  omxpenlem  8869  mapen  8937  f1finf1o  9055  unirnffid  9120  fdmfifsupp  9147  mapfien  9176  intrnfi  9184  marypha2  9207  ordtypelem7  9292  wemapsolem  9318  wemapso  9319  wemapso2lem  9320  unxpwdom2  9356  ixpiunwdom  9358  cantnfle  9438  cantnfp1lem2  9446  cantnfp1lem3  9447  cantnfp1  9448  oemapvali  9451  cantnflem1a  9452  cantnflem1c  9454  cantnflem3  9458  cantnf  9460  cnfcomlem  9466  cnfcom3  9471  updjudhcoinlf  9699  updjudhcoinrg  9700  fseqenlem1  9789  numacn  9814  infpwfien  9827  isf32lem2  10119  isf34lem7  10144  isf34lem6  10145  unirnfdomd  10332  ofsubeq0  11979  ofnegsub  11980  ofsubge0  11981  seqf1olem2  13772  resunimafz0  14166  wrdfn  14240  swrdvalfn  14373  pfxfn  14403  pfxid  14406  cats1un  14443  cshwfn  14523  ccatco  14557  limsupgle  15195  o1of2  15331  o1rlimmul  15337  isercolllem2  15386  isercoll  15388  isercoll2  15389  climsup  15390  fsumss  15446  ruclem11  15958  vdwlem2  16692  vdwlem6  16696  vdwlem9  16699  vdwlem12  16702  0ram  16730  ramub1lem1  16736  pwsle  17212  pwsleval  17213  pwsvscaval  17215  mrcuni  17339  mrcun  17340  invf1o  17490  funcres2c  17626  setcmon  17811  setcepi  17812  uncfcurf  17966  yoniso  18012  isacs4lem  18271  acsmapd  18281  gsumval2  18379  prdsplusgcl  18425  prdsidlem  18426  prdsmndd  18427  mhmf1o  18449  resmhm2b  18470  mhmima  18472  mhmeql  18473  prdspjmhm  18476  pwsco1mhm  18479  pwsco2mhm  18480  gsumwmhm  18493  frmdss2  18511  grpinvf1o  18654  prdsinvlem  18693  cycsubgcl  18834  ghmrn  18856  ghmpreima  18865  ghmeql  18866  ghmnsgima  18867  ghmnsgpreima  18868  ghmeqker  18870  ghmf1o  18873  gass  18916  cntzmhm  18954  symgextres  19042  gsmsymgrfixlem1  19044  fvcosymgeq  19046  f1omvdconj  19063  pmtrfinv  19078  symgtrinv  19089  pmtr3ncomlem1  19090  sygbasnfpfi  19129  efginvrel2  19342  efgredleme  19358  ghmplusg  19456  prdscmnd  19471  gsumval3a  19513  gsumval3eu  19514  gsumzaddlem  19531  gsumzsplit  19537  gsumpt  19572  prdsgsum  19591  dprdfcntz  19627  dprdfadd  19632  dprdfeq0  19634  dprdf11  19635  dprdlub  19638  dprdspan  19639  dprd2dlem1  19653  dmdprdpr  19661  dprdpr  19662  dpjlem  19663  ablfac1eu  19685  prdsmulrcl  19859  prdsringd  19860  prdscrngd  19861  prds1  19862  rhmf1o  19985  rnrhmsubrg  20065  isabvd  20089  lmodfopnelem1  20168  lcomfsupp  20172  prdsvscacl  20239  prdslmodd  20240  lmhmco  20314  lmhmplusg  20315  lmhmvsca  20316  lmhmf1o  20317  lmhmeql  20326  lspextmo  20327  rrgsupp  20571  pjfo  20931  dsmmbas2  20953  dsmm0cl  20956  dsmmacl  20957  dsmmsubg  20959  dsmmlss  20960  frlmvplusgvalc  20983  frlmvscaval  20984  frlmplusgvalb  20985  frlmvscavalb  20986  frlmsslss2  20991  frlmphllem  20996  frlmphl  20997  frlmssuvc2  21011  frlmsslsp  21012  frlmup1  21014  frlmup2  21015  frlmup3  21016  frlmup4  21017  islindf4  21054  psrbagfsupp  21132  psrbaglesupp  21136  psrbaglesuppOLD  21137  psrbaglecl  21138  psrbagaddcl  21140  psrbagcon  21142  psrbagconOLD  21143  psrbaglefi  21144  psrbaglefiOLD  21145  psrbagconf1o  21148  psrbagconf1oOLD  21149  gsumbagdiaglemOLD  21150  gsumbagdiaglem  21153  psrass1lem  21155  psrvscaval  21170  psrlidm  21181  psrridm  21182  psrass1  21183  psrdi  21184  psrdir  21185  mplsubglem  21214  mplvscaval  21229  subrgmvrf  21244  mplbas2  21252  mvrf2  21277  mplind  21287  psrbagev1  21294  psrbagev1OLD  21295  psrbagev2  21296  evlslem3  21299  evlslem1  21301  evlsvar  21309  mpfind  21326  ismhp3  21342  mhpmulcl  21348  psrplusgpropd  21416  coe1add  21444  coe1addfv  21445  evl1addd  21516  evl1subd  21517  evl1muld  21518  pf1mpf  21527  pf1ind  21530  mamudir  21560  mamulid  21599  mamurid  21600  mdetrlin  21760  mdetrsca  21761  mdetralt  21766  mdetunilem7  21776  mdetunilem9  21778  madurid  21802  cnrest2  22446  lmss  22458  lmcnp  22464  cnt0  22506  cnt1  22510  cnhaus  22514  rncmp  22556  conncn  22586  2ndcomap  22618  1stccnp  22622  comppfsc  22692  1stckgenlem  22713  ptbasfi  22741  ptopn  22743  ptclsg  22775  ptcnp  22782  upxp  22783  txtube  22800  txcmplem1  22801  hauseqlcld  22806  xkohaus  22813  xkoptsub  22814  cnmpt11  22823  cnmpt21  22831  cnmpt22f  22835  cnmptcom  22838  qtopss  22875  qtopeu  22876  qtopomap  22878  qtopcmap  22879  kqffn  22885  hmeof1o2  22923  xkocnv  22974  rnelfm  23113  ptcmplem1  23212  cnextfres1  23228  ghmcnp  23275  tgphaus  23277  prdstmdd  23284  prdstgpd  23285  fmucnd  23453  psmetxrge0  23475  isxmet2d  23489  prdsmet  23532  blelrnps  23578  blelrn  23579  xmetresbl  23599  comet  23678  stdbdxmet  23680  met2ndci  23687  prdsxmslem2  23694  isngp3  23763  nmotri  23912  metdsre  24025  bndth  24130  evth  24131  fmcfil  24445  bcthlem4  24500  rrxcph  24565  rrxds  24566  rrxmet  24581  evthicc2  24633  ovolfsf  24644  ovolmge0  24650  ovollb2lem  24661  ovolunlem1a  24669  ovoliunlem1  24675  ovoliun  24678  ovoliun2  24679  ovolscalem1  24686  ovolicc1  24689  ovolicc2lem4  24693  ovolicc2  24695  voliunlem1  24723  voliunlem3  24725  volsup  24729  ioombl1lem2  24732  ioombl1lem4  24734  uniiccdif  24751  uniioombllem2  24756  uniioombllem3  24758  uniioombllem6  24761  volsup2  24778  vitalilem4  24784  mbfeqalem1  24814  mbfmulc2lem  24820  mbfmax  24822  mbfaddlem  24833  mbfadd  24834  mbfsub  24835  mbfsup  24837  mbfinf  24838  itg1ge0  24859  itg1addlem1  24865  i1faddlem  24866  i1fmullem  24867  i1fadd  24868  i1fmul  24869  itg1addlem4  24872  itg1addlem4OLD  24873  i1fmulclem  24876  i1fmulc  24877  itg1mulc  24878  i1fres  24879  itg10a  24884  itg1ge0a  24885  itg1lea  24886  mbfi1fseqlem3  24891  mbfi1fseqlem4  24892  mbfi1flimlem  24896  mbfmullem2  24898  mbfmul  24900  itg20  24911  itg2lea  24918  itg2splitlem  24922  itg2split  24923  itg2monolem1  24924  itg2monolem2  24925  itg2monolem3  24926  itg2mono  24927  itg2i1fseqle  24928  itg2i1fseq  24929  itg2addlem  24932  itg2gt0  24934  itg2cnlem1  24935  itg2cnlem2  24936  itg2cn  24937  itgitg1  24982  bddmulibl  25012  bddibl  25013  dvidlem  25088  dvaddbr  25111  dvmulbr  25112  dvaddf  25115  dvcmulf  25118  dvrec  25128  dvcnvlem  25149  rolle  25163  dveq0  25173  dv11cn  25174  dvivthlem2  25182  dvivth  25183  dvne0  25184  lhop1lem  25186  lhop1  25187  lhop2  25188  lhop  25189  ftc1cn  25216  tdeglem1  25229  tdeglem3  25231  tdeglem4  25233  tdeglem4OLD  25234  mdegleb  25238  mdegldg  25240  mdegaddle  25248  ply1remlem  25336  ply1rem  25337  fta1glem1  25339  fta1glem2  25340  fta1blem  25342  plyeq0lem  25380  plyeq0  25381  plyaddlem1  25383  coeeulem  25394  coeaddlem  25419  coemulc  25425  dgradd2  25438  dgrcolem2  25444  ofmulrt  25451  plyrem  25474  vieta1lem1  25479  vieta1  25481  plyexmo  25482  elqaalem3  25490  aannenlem1  25497  aalioulem2  25502  ulmuni  25560  ulmdvlem1  25568  ulmdv  25571  mbfulm  25574  iblulm  25575  itgulm  25576  rlimcnp2  26125  jensen  26147  amgm  26149  basellem3  26241  basellem7  26245  basellem9  26247  dchrelbas2  26394  dchrmulcl  26406  dchrfi  26412  dchreq  26415  dchrresb  26416  dchrinv  26418  dchr1re  26420  sumdchr2  26427  dchr2sum  26430  lgsqrlem2  26504  lgsqrlem3  26505  rpvmasum2  26669  dchrisum0re  26670  mirf1o  27039  lmif1o  27165  eqeefv  27280  axlowdimlem14  27332  vtxdgfisf  27852  2pthon3v  28317  nvinvfval  29011  sspg  29099  ssps  29101  sspmlem  29103  sspn  29107  lnon0  29169  ubthlem1  29241  pjfn  30080  kbpj  30327  kbass2  30488  elpjrn  30561  ofrn2  30986  off2  30987  ofresid  30988  xppreima2  30997  ofpreima2  31012  suppovss  31026  resf1o  31074  swrdrn3  31236  pwrssmgc  31287  mgcf1o  31290  gsumhashmul  31325  gsumle  31359  symgcom2  31362  pmtrcnel  31367  pmtrcnel2  31368  pmtrcnelor  31369  cycpmfvlem  31388  cycpmfv3  31391  cycpmcl  31392  cycpmco2rn  31401  cycpmco2  31409  cycpm3cl2  31412  cyc3co2  31416  cyc3evpm  31426  islinds5  31572  ellspds  31573  rhmpreimaidl  31612  elrspunidl  31615  rhmimaidl  31618  rhmpreimaprmidl  31636  dimkerim  31717  fedgmullem2  31720  fedgmul  31721  cmpcref  31809  rhmpreimacnlem  31843  fsumcvg4  31909  pl1cn  31914  qqhval2lem  31940  prodindf  32000  indpreima  32002  esumcvg  32063  ofcf  32080  ofcof  32084  measfn  32181  meascnbl  32196  sibfof  32316  sitgaddlemb  32324  subiwrdlen  32362  rrvfn  32421  plymul02  32534  signsplypnf  32538  signsply0  32539  reprsuc  32604  reprdifc  32616  breprexplema  32619  circlemethhgt  32632  hgt750lemb  32645  f1resrcmplf1dlem  33067  pthhashvtx  33098  cvmopnlem  33249  cvmliftmolem1  33252  cvmliftlem10  33265  cvmlift2lem9a  33274  cvmlift2lem6  33279  cvmlift2lem12  33285  cvmliftphtlem  33288  cvmlift3lem9  33298  mrsubrn  33484  elmrsubrn  33491  elmsubrn  33499  msubrn  33500  mclsind  33541  mclsppslem  33554  mclspps  33555  iprodefisumlem  33715  matunitlindflem1  35782  poimirlem1  35787  poimirlem2  35788  poimirlem3  35789  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem22  35808  poimirlem23  35809  poimirlem29  35815  poimirlem30  35816  poimirlem31  35817  poimir  35819  mblfinlem2  35824  itg2addnclem3  35839  itg2addnc  35840  itg2gt0cn  35841  ftc1cnnc  35858  ftc1anclem5  35863  ftc1anclem7  35865  ftc1anc  35867  sdclem2  35909  istotbnd3  35938  sstotbnd2  35941  isbnd3  35951  heibor1lem  35976  rrnmet  35996  grpokerinj  36060  isdrngo2  36125  lfl1  37091  lfladdcl  37092  lflvscl  37098  lkr0f  37115  lkrsc  37118  eqlkr2  37121  eqlkr3  37122  ldualvaddval  37152  ldualvsval  37159  tendoeq1  38785  sticksstones1  40109  sticksstones2  40110  sticksstones3  40111  sticksstones12a  40120  sticksstones12  40121  metakunt19  40150  metakunt25  40156  metakunt33  40164  frlmvscadiccat  40244  frlmsnic  40270  pwspjmhmmgpd  40274  pwsgprod  40276  evlsbagval  40282  evlsaddval  40284  evlsmulval  40285  fsuppssind  40289  mhphf  40292  ismrcd1  40527  ismrcd2  40528  istopclsd  40529  isnacs3  40539  mzpaddmpt  40570  mzpmulmpt  40571  mzpsubst  40577  mzpcong  40801  fnwe2lem2  40883  islmodfg  40901  kercvrlsm  40915  dgrsub2  40967  mpaaeu  40982  rngunsnply  41005  idomrootle  41027  hausgraph  41044  fsovf1od  41631  brcoffn  41647  clsneiel1  41725  wfximgfd  41781  extoimad  41782  mnringmulrcld  41853  mnurndlem1  41906  caofcan  41948  ofmul12  41950  ofdivrec  41951  ofdivcan4  41952  ofdivdiv2  41953  dvconstbi  41959  binomcxplemnotnn0  41981  refsum2cnlem1  42587  ssmapsn  42763  preimaiocmnf  43106  fsumsupp0  43126  fsumsermpt  43127  climinf  43154  climinf2lem  43254  limsupmnflem  43268  limsupvaluz2  43286  supcnvlimsup  43288  limsupgtlem  43325  liminfvalxr  43331  liminflelimsupuz  43333  xlimconst2  43383  climxlim2  43394  icccncfext  43435  dvnprodlem1  43494  volicoff  43543  voliooicof  43544  fourierdlem25  43680  etransclem2  43784  etransclem35  43817  fge0iccico  43915  sge0tsms  43925  sge0sup  43936  sge0resrn  43949  sge0le  43952  sge0fodjrnlem  43961  sge0isum  43972  sge0seq  43991  nnfoctbdjlem  44000  meadjiunlem  44010  omeiunle  44062  hoicvr  44093  ovolval4lem1  44194  ovolval5lem3  44199  ovnovollem1  44201  ovnovollem2  44202  iinhoiicclem  44218  iunhoiioolem  44220  preimaicomnf  44256  smfresal  44333  smfsuplem1  44355  smflimsuplem2  44365  fcoreslem3  44570  fcoreslem4  44571  fcores  44572  mgmhmf1o  45352  resmgmhm2b  45365  mgmhmima  45367  mgmhmeql  45368  rnghmf1o  45472  ackvalsucsucval  46045  amgmwlem  46517