Theorem ffnd 6710

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

This proof depends on syntax axioms:   → wi 4   Fn wfn 6535  ⟶wf 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-f 6544

This theorem is used by:  fnconstg  6770  f1fn  6779  fofn  6798  f1ofn  6825  feqmptd  6953  fssrescdmd  7126  fprb  7196  f1resrcmplf1dlem  7274  cocan1  7295  oprres  7584  off  7698  coof  7704  ofco  7705  caofref  7711  caofid0l  7713  caofid0r  7714  caofid1  7715  caofid2  7716  caofrss  7719  caoftrn  7721  fo2ndf  8118  fnwelem  8129  fnse  8131  suppsnop  8176  suppss  8192  suppssr  8193  suppssrg  8194  suppssof1  8197  suppofssd  8201  suppofss1d  8202  suppofss2d  8203  suppcoss  8205  smocdmdom  8357  elmapfn  8864  ralxpmap  8896  omxpenlem  9069  mapen  9132  f1finf1o  9236  unirnffid  9307  fdmfifsupp  9338  mapfien  9371  intrnfi  9379  marypha2  9402  ordtypelem7  9489  wemapsolem  9515  wemapso  9516  wemapso2lem  9517  unxpwdom2  9553  ixpiunwdom  9555  cantnfle  9643  cantnfp1lem2  9651  cantnfp1lem3  9652  cantnfp1  9653  oemapvali  9656  cantnflem1a  9657  cantnflem1c  9659  cantnflem3  9663  cantnf  9665  cnfcomlem  9671  cnfcom3  9676  updjudhcoinlf  9930  updjudhcoinrg  9931  fseqenlem1  10020  numacn  10045  infpwfien  10058  isf32lem2  10349  isf34lem7  10374  isf34lem6  10375  unirnfdomd  10563  ofsubeq0  12226  ofnegsub  12227  ofsubge0  12228  seqf1olem2  14091  resunimafz0  14495  wrdfn  14578  swrdvalfn  14705  swrdrn3  14707  pfxfn  14736  pfxid  14739  cats1un  14775  cshwfn  14857  ccatco  14891  limsupgle  15547  o1of2  15683  o1rlimmul  15689  isercolllem2  15736  isercoll  15738  isercoll2  15739  climsup  15740  fsumss  15794  ruclem11  16313  vdwlem2  17059  vdwlem6  17063  vdwlem9  17066  vdwlem12  17069  0ram  17097  ramub1lem1  17103  pwsle  17563  pwsleval  17564  pwsvscaval  17566  mrcuni  17694  mrcun  17695  invf1o  17843  funcres2c  17977  setcmon  18161  setcepi  18162  uncfcurf  18312  yoniso  18358  isacs4lem  18617  acsmapd  18627  chnso  18697  gsumval2  18765  mgmhmf1o  18779  resmgmhm2b  18792  mgmhmima  18794  mgmhmeql  18795  prdsplusgsgrpcl  18811  prdssgrpd  18812  prdsplusgcl  18849  prdsidlem  18850  prdsmndd  18851  mhmf1o  18877  resmhm2b  18904  mhmimalem  18906  mhmima  18907  mhmeql  18908  prdspjmhm  18911  pwsco1mhm  18914  pwsco2mhm  18915  gsumwmhm  18927  frmdss2  18945  grpinvf1o  19098  prdsinvlem  19138  cycsubgcl  19300  ghmrn  19322  ghmpreima  19331  ghmeql  19332  ghmnsgima  19333  ghmnsgpreima  19334  ghmeqker  19336  ghmf1o  19341  ghmqusnsglem1  19373  ghmqusnsg  19375  ghmquskerlem1  19376  ghmquskerco  19377  ghmquskerlem3  19379  ghmqusker  19380  gass  19394  cntzmhm  19434  symgextres  19518  gsmsymgrfixlem1  19520  fvcosymgeq  19522  f1omvdconj  19539  pmtrfinv  19554  symgtrinv  19565  pmtr3ncomlem1  19566  sygbasnfpfi  19605  efginvrel2  19820  efgredleme  19836  ghmplusg  19939  prdscmnd  19954  gsumval3a  19996  gsumval3eu  19997  gsumzaddlem  20014  gsumzsplit  20020  gsumpt  20055  prdsgsum  20074  dprdfcntz  20110  dprdfadd  20115  dprdfeq0  20117  dprdf11  20118  dprdlub  20121  dprdspan  20122  dprd2dlem1  20136  dmdprdpr  20144  dprdpr  20145  dpjlem  20146  ablfac1eu  20168  gsumle  20238  prdsmulrngcl  20276  prdsrngd  20277  prdsringd  20427  prdscrngd  20428  prds1  20429  pwspjmhmmgpd  20434  pwsgprod  20436  rnghmf1o  20559  rhmf1o  20604  rhmimasubrnglem  20693  rnrhmsubrg  20733  rrgsupp  20829  imadrhmcl  20929  isabvd  20944  lmodfopnelem1  21048  lcomfsupp  21052  prdsvscacl  21118  prdslmodd  21119  lmhmco  21193  lmhmplusg  21194  lmhmvsca  21195  lmhmf1o  21196  lmhmeql  21205  lspextmo  21206  rhmpreimaidl  21445  rhmpreimaprmidl  21508  pjfo  21894  dsmmbas2  21916  dsmm0cl  21919  dsmmacl  21920  dsmmsubg  21922  dsmmlss  21923  frlmvplusgvalc  21946  frlmvscaval  21947  frlmplusgvalb  21948  frlmvscavalb  21949  frlmsslss2  21954  frlmphllem  21959  frlmphl  21960  frlmssuvc2  21974  frlmsslsp  21975  frlmup1  21977  frlmup2  21978  frlmup3  21979  frlmup4  21980  islindf4  22017  psrbagfsupp  22098  psrbaglesupp  22101  psrbaglecl  22102  psrbagaddcl  22103  psrbagcon  22104  psrbaglefi  22105  psrbagleadd1  22107  psrbagconf1o  22108  gsumbagdiaglem  22110  psrass1lem  22112  psrvscaval  22129  psrlidm  22140  psrridm  22141  psrass1  22142  psrdi  22143  psrdir  22144  psrascl  22157  mvrf2  22171  mplsubglem  22177  mplvscaval  22194  subrgmvrf  22214  mplbas2  22222  mplind  22250  psrbagev1  22257  psrbagev2  22258  evlslem3  22260  evlslem1  22262  evlsvvval  22273  evlsvar  22275  evladdval  22283  evlmulval  22284  mpfind  22295  mplmapghm  22302  evlsaddval  22309  evlsmulval  22310  selvvvval  22322  ismhp3  22334  mhpmulcl  22341  psdmplcl  22354  psdadd  22355  psdvsca  22356  psdmul  22358  psdmvr  22361  psrplusgpropd  22424  coe1add  22454  coe1addfv  22455  evl1addd  22530  evl1subd  22531  evl1muld  22532  pf1mpf  22541  pf1ind  22544  evls1fpws  22558  ressply1evl  22559  rhmply1vsca  22574  mamudir  22590  mamulid  22627  mamurid  22628  mdetrlin  22788  mdetrsca  22789  mdetralt  22794  mdetunilem7  22804  mdetunilem9  22806  madurid  22830  cnrest2  23472  lmss  23484  lmcnp  23490  cnt0  23532  cnt1  23536  cnhaus  23540  rncmp  23582  conncn  23612  2ndcomap  23644  1stccnp  23648  comppfsc  23718  1stckgenlem  23739  ptbasfi  23767  ptopn  23769  ptclsg  23801  ptcnp  23808  upxp  23809  txtube  23826  txcmplem1  23827  hauseqlcld  23832  xkohaus  23839  xkoptsub  23840  cnmpt11  23849  cnmpt21  23857  cnmpt22f  23861  cnmptcom  23864  qtopss  23901  qtopeu  23902  qtopomap  23904  qtopcmap  23905  kqffn  23911  hmeof1o2  23949  xkocnv  24000  rnelfm  24139  ptcmplem1  24238  cnextfres1  24254  ghmcnp  24301  tgphaus  24303  prdstmdd  24310  prdstgpd  24311  fmucnd  24477  psmetxrge0  24499  isxmet2d  24513  prdsmet  24556  blelrnps  24602  blelrn  24603  xmetresbl  24623  comet  24699  stdbdxmet  24701  met2ndci  24708  prdsxmslem2  24715  isngp3  24784  nmotri  24925  metdsre  25040  bndth  25146  evth  25147  fmcfil  25460  bcthlem4  25515  rrxcph  25580  rrxds  25581  rrxmet  25596  evthicc2  25648  ovolfsf  25659  ovolmge0  25665  ovollb2lem  25676  ovolunlem1a  25684  ovoliunlem1  25690  ovoliun  25693  ovoliun2  25694  ovolscalem1  25701  ovolicc1  25704  ovolicc2lem4  25708  ovolicc2  25710  voliunlem1  25738  voliunlem3  25740  volsup  25744  ioombl1lem2  25747  ioombl1lem4  25749  uniiccdif  25766  uniioombllem2  25771  uniioombllem3  25773  uniioombllem6  25776  volsup2  25793  vitalilem4  25799  mbfeqalem1  25829  mbfmulc2lem  25835  mbfmax  25837  mbfaddlem  25848  mbfadd  25849  mbfsub  25850  mbfsup  25852  mbfinf  25853  itg1ge0  25874  itg1addlem1  25880  i1faddlem  25881  i1fmullem  25882  i1fadd  25883  i1fmul  25884  itg1addlem4  25887  i1fmulclem  25890  i1fmulc  25891  itg1mulc  25892  i1fres  25893  itg10a  25898  itg1ge0a  25899  itg1lea  25900  mbfi1fseqlem3  25905  mbfi1fseqlem4  25906  mbfi1flimlem  25910  mbfmullem2  25912  mbfmul  25914  itg20  25925  itg2lea  25932  itg2splitlem  25936  itg2split  25937  itg2monolem1  25938  itg2monolem2  25939  itg2monolem3  25940  itg2mono  25941  itg2i1fseqle  25942  itg2i1fseq  25943  itg2addlem  25946  itg2gt0  25948  itg2cnlem1  25949  itg2cnlem2  25950  itg2cn  25951  itgitg1  25997  bddmulibl  26027  bddibl  26028  dvidlem  26103  dvaddbr  26126  dvmulbr  26127  dvaddf  26130  dvcmulf  26133  dvrec  26143  dvcnvlem  26164  rolle  26178  dveq0  26188  dv11cn  26189  dvivthlem2  26197  dvivth  26198  dvne0  26199  lhop1lem  26201  lhop1  26202  lhop2  26203  lhop  26204  ftc1cn  26231  tdeglem1  26244  tdeglem3  26245  tdeglem4  26246  mdegleb  26250  mdegldg  26252  mdegaddle  26260  ply1remlem  26351  ply1rem  26352  fta1glem1  26354  fta1glem2  26355  fta1blem  26357  idomrootle  26359  plyeq0lem  26396  plyeq0  26397  plyaddlem1  26399  coeeulem  26410  coeaddlem  26435  coemulc  26441  dgradd2  26454  dgrcolem2  26460  ofmulrt  26469  plymul02  26470  plyrem  26495  vieta1lem1  26500  vieta1  26502  plyexmo  26503  elqaalem3  26511  aannenlem1  26520  aalioulem2  26525  ulmuni  26584  ulmdvlem1  26592  ulmdv  26595  mbfulm  26598  iblulm  26599  itgulm  26600  rlimcnp2  27160  jensen  27182  amgm  27184  basellem3  27276  basellem7  27280  basellem9  27282  dchrelbas2  27430  dchrmulcl  27442  dchrfi  27448  dchreq  27451  dchrresb  27452  dchrinv  27454  dchr1re  27456  sumdchr2  27463  dchr2sum  27466  lgsqrlem2  27540  lgsqrlem3  27541  rpvmasum2  27705  dchrisum0re  27706  mirf1o  28975  lmif1o  29133  eqeefv  29282  axlowdimlem14  29334  vtxdgfisf  29855  2pthon3v  30321  nvinvfval  31021  sspg  31109  ssps  31111  sspmlem  31113  sspn  31117  lnon0  31179  ubthlem1  31251  pjfn  32090  kbpj  32337  kbass2  32498  elpjrn  32571  ofrn2  33014  off2  33015  ofresid  33016  xppreima2  33025  ofpreima2  33040  suppovss  33055  resf1o  33104  prodindf  33211  indpreima  33214  pwrssmgc  33343  mgcf1o  33346  gsumfs2d  33404  gsumhashmul  33410  symgcom2  33427  pmtrcnel  33432  pmtrcnel2  33433  pmtrcnelor  33434  cycpmfvlem  33455  cycpmfv3  33458  cycpmcl  33459  cycpmco2rn  33468  cycpmco2  33476  cycpm3cl2  33479  cyc3co2  33483  cyc3evpm  33493  elrgspnlem1  33585  elrgspnlem2  33586  elrgspnlem4  33588  elrgspnsubrunlem1  33590  elrgspnsubrunlem2  33591  gsumind  33688  islinds5  33705  ellspds  33706  elrspunidl  33759  elrspunsn  33760  rhmimaidl  33763  rprmdvdsprod  33847  1arithidomlem2  33849  evls1fn  33873  ply1dg1rt  33893  ply1mulrtss  33895  ply1degltel  33907  ply1degleel  33908  ply1degltlss  33909  ply1gsumz  33912  ig1pmindeg  33915  r1pquslmic  33923  0mplrim  33927  mplasclco  33929  selvply1rhmlema  33931  selvply1rhmlemb  33932  selvply1rhmlem1  33933  selvply1rhmlem4  33936  selvply1rhm0  33939  extvfvcl  33949  mplmulmvr  33952  evlextv  33955  mplvrpmmhm  33959  mplvrpmrhm  33960  psrmonprod  33965  esplyfval0  33977  esplyfval2  33978  esplyfv1  33982  esplyfv  33983  esplyfval3  33985  esplyfvaln  33987  esplyind  33988  vieta  33993  exsslsb  34010  ply1degltdimlem  34035  ply1degltdim  34036  dimkerim  34040  fedgmullem2  34043  fedgmul  34044  lvecendof1f1o  34046  fldextrspunlsplem  34086  fldextrspunlsp  34087  irngss  34100  irngnzply1  34104  extdgfialglem2  34106  irngnminplynz  34125  2sqr3minply  34193  cos9thpiminply  34201  cmpcref  34263  rhmpreimacnlem  34297  fsumcvg4  34363  pl1cn  34368  qqhval2lem  34394  esumcvg  34499  ofcf  34516  ofcof  34520  measfn  34618  meascnbl  34633  sibfof  34754  sitgaddlemb  34762  subiwrdlen  34800  rrvfn  34859  signsplypnf  34961  signsply0  34962  reprsuc  35026  reprdifc  35038  breprexplema  35041  circlemethhgt  35054  hgt750lemb  35067  pthhashvtx  35633  cvmopnlem  35783  cvmliftmolem1  35786  cvmliftlem10  35799  cvmlift2lem9a  35808  cvmlift2lem6  35813  cvmlift2lem12  35819  cvmliftphtlem  35822  cvmlift3lem9  35832  mrsubrn  36018  elmrsubrn  36025  elmsubrn  36033  msubrn  36034  mclsind  36075  mclsppslem  36088  mclspps  36089  iprodefisumlem  36245  weiunfrlem  37008  mh-inf3f1  37085  matunitlindflem1  38300  poimirlem1  38305  poimirlem2  38306  poimirlem3  38307  poimirlem16  38320  poimirlem17  38321  poimirlem19  38323  poimirlem20  38324  poimirlem22  38326  poimirlem23  38327  poimirlem29  38333  poimirlem30  38334  poimirlem31  38335  poimir  38337  mblfinlem2  38342  itg2addnclem3  38357  itg2addnc  38358  itg2gt0cn  38359  ftc1cnnc  38376  ftc1anclem5  38381  ftc1anclem7  38383  ftc1anc  38385  sdclem2  38426  istotbnd3  38455  sstotbnd2  38458  isbnd3  38468  heibor1lem  38493  rrnmet  38513  grpokerinj  38577  isdrngo2  38642  lfl1  39877  lfladdcl  39878  lflvscl  39884  lkr0f  39901  lkrsc  39904  eqlkr2  39907  eqlkr3  39908  ldualvaddval  39938  ldualvsval  39945  tendoeq1  41571  zndvdchrrhm  42773  hashscontpow  42922  aks6d1c3  42923  aks6d1c2lem4  42927  aks6d1c2  42930  sticksstones1  42946  sticksstones2  42947  sticksstones3  42948  sticksstones12a  42957  sticksstones12  42958  aks6d1c6lem2  42971  aks6d1c6lem3  42972  aks6d1c6isolem1  42974  aks6d1c6isolem3  42976  aks6d1c6lem5  42977  aks6d1c7lem1  42980  unitscyglem1  42995  dvun  43153  frlmvscadiccat  43313  fiabv  43337  frlmsnic  43341  evlselvlem  43353  evlselv  43354  fsuppssind  43358  mhphf  43362  ismrcd1  43462  ismrcd2  43463  istopclsd  43464  isnacs3  43474  mzpaddmpt  43505  mzpmulmpt  43506  mzpsubst  43512  mzpcong  43732  fnwe2lem2  43811  islmodfg  43829  kercvrlsm  43843  dgrsub2  43895  mpaaeu  43910  rngunsnply  43929  hausgraph  43965  ofoafg  44114  ofoafo  44116  ofoaid1  44118  ofoaid2  44119  naddcnff  44122  naddcnffn  44123  naddcnffo  44124  naddcnfcom  44126  naddcnfid1  44127  naddcnfass  44129  fsovf1od  44775  brcoffn  44789  clsneiel1  44867  wfximgfd  44922  extoimad  44923  mnringmulrcld  44985  mnurndlem1  45024  caofcan  45066  ofmul12  45068  ofdivrec  45069  ofdivcan4  45070  ofdivdiv2  45071  dvconstbi  45077  binomcxplemnotnn0  45099  relpmin  45694  refsum2cnlem1  45790  ssmapsn  45965  preimaiocmnf  46309  fsumsupp0  46327  fsumsermpt  46328  climinf  46355  climinf2lem  46453  limsupmnflem  46467  limsupvaluz2  46485  supcnvlimsup  46487  limsupgtlem  46524  liminfvalxr  46530  liminflelimsupuz  46532  xlimconst2  46582  climxlim2  46593  icccncfext  46634  dvnprodlem1  46693  volicoff  46742  voliooicof  46743  fourierdlem25  46879  fourierdlem48  46901  fourierdlem49  46902  etransclem2  46983  etransclem35  47016  fge0iccico  47117  sge0tsms  47127  sge0sup  47138  sge0resrn  47151  sge0le  47154  sge0fodjrnlem  47163  sge0isum  47174  sge0seq  47193  nnfoctbdjlem  47202  meadjiunlem  47212  omeiunle  47264  hoicvr  47295  ovolval4lem1  47396  ovolval5lem3  47401  ovnovollem1  47403  ovnovollem2  47404  iinhoiicclem  47420  iunhoiioolem  47422  preimaicomnf  47458  smfresal  47535  smfsuplem1  47558  smflimsuplem2  47568  fcoreslem3  47835  fcoreslem4  47836  fcores  47837  isubgredg  48664  upgrimpths  48707  ackvalsucsucval  49501  funchomf  49908  imasubc  49962  imassc  49964  imaid  49965  prcofdiag1  50204  prcofdiag  50205  oppfdiag1  50225  oppfdiag  50227  amgmwlem  50683