Theorem ffnd 6715

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

Syntax hints:   → wi 4   Fn wfn 6535  ⟶wf 6536

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 398  df-f 6544

This theorem is referenced by:  fnconstg  6776  f1fn  6785  fofn  6804  f1ofn  6831  feqmptd  6956  fprb  7190  rnmptcOLD  7204  cocan1  7284  oprres  7570  off  7683  ofco  7688  caofref  7694  caofid0l  7696  caofid0r  7697  caofid1  7698  caofid2  7699  caofrss  7701  caoftrn  7703  fo2ndf  8102  fnwelem  8112  fnse  8114  suppsnop  8158  suppss  8174  suppssOLD  8175  suppssr  8176  suppssrg  8177  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  12205  ofnegsub  12206  ofsubge0  12207  seqf1olem2  14004  resunimafz0  14400  wrdfn  14474  swrdvalfn  14597  pfxfn  14627  pfxid  14630  cats1un  14667  cshwfn  14747  ccatco  14782  limsupgle  15417  o1of2  15553  o1rlimmul  15559  isercolllem2  15608  isercoll  15610  isercoll2  15611  climsup  15612  fsumss  15667  ruclem11  16179  vdwlem2  16911  vdwlem6  16915  vdwlem9  16918  vdwlem12  16921  0ram  16949  ramub1lem1  16955  pwsle  17434  pwsleval  17435  pwsvscaval  17437  mrcuni  17561  mrcun  17562  invf1o  17712  funcres2c  17848  setcmon  18033  setcepi  18034  uncfcurf  18188  yoniso  18234  isacs4lem  18493  acsmapd  18503  gsumval2  18601  prdsplusgsgrpcl  18619  prdssgrpd  18620  prdsplusgcl  18652  prdsidlem  18653  prdsmndd  18654  mhmf1o  18678  resmhm2b  18699  mhmimalem  18701  mhmima  18702  mhmeql  18703  prdspjmhm  18706  pwsco1mhm  18709  pwsco2mhm  18710  gsumwmhm  18722  frmdss2  18740  grpinvf1o  18889  prdsinvlem  18928  cycsubgcl  19077  ghmrn  19099  ghmpreima  19108  ghmeql  19109  ghmnsgima  19110  ghmnsgpreima  19111  ghmeqker  19113  ghmf1o  19116  gass  19159  cntzmhm  19198  symgextres  19286  gsmsymgrfixlem1  19288  fvcosymgeq  19290  f1omvdconj  19307  pmtrfinv  19322  symgtrinv  19333  pmtr3ncomlem1  19334  sygbasnfpfi  19373  efginvrel2  19588  efgredleme  19604  ghmplusg  19706  prdscmnd  19721  gsumval3a  19763  gsumval3eu  19764  gsumzaddlem  19781  gsumzsplit  19787  gsumpt  19822  prdsgsum  19841  dprdfcntz  19877  dprdfadd  19882  dprdfeq0  19884  dprdf11  19885  dprdlub  19888  dprdspan  19889  dprd2dlem1  19903  dmdprdpr  19911  dprdpr  19912  dpjlem  19913  ablfac1eu  19935  prdsmulrcl  20123  prdsringd  20124  prdscrngd  20125  prds1  20126  pwspjmhmmgpd  20131  rhmf1o  20258  rnrhmsubrg  20385  imadrhmcl  20401  isabvd  20416  lmodfopnelem1  20496  lcomfsupp  20500  prdsvscacl  20567  prdslmodd  20568  lmhmco  20642  lmhmplusg  20643  lmhmvsca  20644  lmhmf1o  20645  lmhmeql  20654  lspextmo  20655  rrgsupp  20894  pjfo  21254  dsmmbas2  21276  dsmm0cl  21279  dsmmacl  21280  dsmmsubg  21282  dsmmlss  21283  frlmvplusgvalc  21306  frlmvscaval  21307  frlmplusgvalb  21308  frlmvscavalb  21309  frlmsslss2  21314  frlmphllem  21319  frlmphl  21320  frlmssuvc2  21334  frlmsslsp  21335  frlmup1  21337  frlmup2  21338  frlmup3  21339  frlmup4  21340  islindf4  21377  psrbagfsupp  21455  psrbaglesupp  21459  psrbaglesuppOLD  21460  psrbaglecl  21461  psrbagaddcl  21463  psrbagcon  21465  psrbagconOLD  21466  psrbaglefi  21467  psrbaglefiOLD  21468  psrbagconf1o  21471  psrbagconf1oOLD  21472  gsumbagdiaglemOLD  21473  gsumbagdiaglem  21476  psrass1lem  21478  psrvscaval  21493  psrlidm  21505  psrridm  21506  psrass1  21507  psrdi  21508  psrdir  21509  mvrf2  21534  mplsubglem  21540  mplvscaval  21557  subrgmvrf  21571  mplbas2  21579  mplind  21613  psrbagev1  21620  psrbagev1OLD  21621  psrbagev2  21622  evlslem3  21625  evlslem1  21627  evlsvar  21635  mpfind  21652  ismhp3  21668  mhpmulcl  21674  psrplusgpropd  21740  coe1add  21768  coe1addfv  21769  evl1addd  21842  evl1subd  21843  evl1muld  21844  pf1mpf  21853  pf1ind  21856  mamudir  21886  mamulid  21925  mamurid  21926  mdetrlin  22086  mdetrsca  22087  mdetralt  22092  mdetunilem7  22102  mdetunilem9  22104  madurid  22128  cnrest2  22772  lmss  22784  lmcnp  22790  cnt0  22832  cnt1  22836  cnhaus  22840  rncmp  22882  conncn  22912  2ndcomap  22944  1stccnp  22948  comppfsc  23018  1stckgenlem  23039  ptbasfi  23067  ptopn  23069  ptclsg  23101  ptcnp  23108  upxp  23109  txtube  23126  txcmplem1  23127  hauseqlcld  23132  xkohaus  23139  xkoptsub  23140  cnmpt11  23149  cnmpt21  23157  cnmpt22f  23161  cnmptcom  23164  qtopss  23201  qtopeu  23202  qtopomap  23204  qtopcmap  23205  kqffn  23211  hmeof1o2  23249  xkocnv  23300  rnelfm  23439  ptcmplem1  23538  cnextfres1  23554  ghmcnp  23601  tgphaus  23603  prdstmdd  23610  prdstgpd  23611  fmucnd  23779  psmetxrge0  23801  isxmet2d  23815  prdsmet  23858  blelrnps  23904  blelrn  23905  xmetresbl  23925  comet  24004  stdbdxmet  24006  met2ndci  24013  prdsxmslem2  24020  isngp3  24089  nmotri  24238  metdsre  24351  bndth  24456  evth  24457  fmcfil  24771  bcthlem4  24826  rrxcph  24891  rrxds  24892  rrxmet  24907  evthicc2  24959  ovolfsf  24970  ovolmge0  24976  ovollb2lem  24987  ovolunlem1a  24995  ovoliunlem1  25001  ovoliun  25004  ovoliun2  25005  ovolscalem1  25012  ovolicc1  25015  ovolicc2lem4  25019  ovolicc2  25021  voliunlem1  25049  voliunlem3  25051  volsup  25055  ioombl1lem2  25058  ioombl1lem4  25060  uniiccdif  25077  uniioombllem2  25082  uniioombllem3  25084  uniioombllem6  25087  volsup2  25104  vitalilem4  25110  mbfeqalem1  25140  mbfmulc2lem  25146  mbfmax  25148  mbfaddlem  25159  mbfadd  25160  mbfsub  25161  mbfsup  25163  mbfinf  25164  itg1ge0  25185  itg1addlem1  25191  i1faddlem  25192  i1fmullem  25193  i1fadd  25194  i1fmul  25195  itg1addlem4  25198  itg1addlem4OLD  25199  i1fmulclem  25202  i1fmulc  25203  itg1mulc  25204  i1fres  25205  itg10a  25210  itg1ge0a  25211  itg1lea  25212  mbfi1fseqlem3  25217  mbfi1fseqlem4  25218  mbfi1flimlem  25222  mbfmullem2  25224  mbfmul  25226  itg20  25237  itg2lea  25244  itg2splitlem  25248  itg2split  25249  itg2monolem1  25250  itg2monolem2  25251  itg2monolem3  25252  itg2mono  25253  itg2i1fseqle  25254  itg2i1fseq  25255  itg2addlem  25258  itg2gt0  25260  itg2cnlem1  25261  itg2cnlem2  25262  itg2cn  25263  itgitg1  25308  bddmulibl  25338  bddibl  25339  dvidlem  25414  dvaddbr  25437  dvmulbr  25438  dvaddf  25441  dvcmulf  25444  dvrec  25454  dvcnvlem  25475  rolle  25489  dveq0  25499  dv11cn  25500  dvivthlem2  25508  dvivth  25509  dvne0  25510  lhop1lem  25512  lhop1  25513  lhop2  25514  lhop  25515  ftc1cn  25542  tdeglem1  25555  tdeglem3  25557  tdeglem4  25559  tdeglem4OLD  25560  mdegleb  25564  mdegldg  25566  mdegaddle  25574  ply1remlem  25662  ply1rem  25663  fta1glem1  25665  fta1glem2  25666  fta1blem  25668  plyeq0lem  25706  plyeq0  25707  plyaddlem1  25709  coeeulem  25720  coeaddlem  25745  coemulc  25751  dgradd2  25764  dgrcolem2  25770  ofmulrt  25777  plyrem  25800  vieta1lem1  25805  vieta1  25807  plyexmo  25808  elqaalem3  25816  aannenlem1  25823  aalioulem2  25828  ulmuni  25886  ulmdvlem1  25894  ulmdv  25897  mbfulm  25900  iblulm  25901  itgulm  25902  rlimcnp2  26451  jensen  26473  amgm  26475  basellem3  26567  basellem7  26571  basellem9  26573  dchrelbas2  26720  dchrmulcl  26732  dchrfi  26738  dchreq  26741  dchrresb  26742  dchrinv  26744  dchr1re  26746  sumdchr2  26753  dchr2sum  26756  lgsqrlem2  26830  lgsqrlem3  26831  rpvmasum2  26995  dchrisum0re  26996  mirf1o  27900  lmif1o  28026  eqeefv  28141  axlowdimlem14  28193  vtxdgfisf  28713  2pthon3v  29177  nvinvfval  29871  sspg  29959  ssps  29961  sspmlem  29963  sspn  29967  lnon0  30029  ubthlem1  30101  pjfn  30940  kbpj  31187  kbass2  31348  elpjrn  31421  ofrn2  31843  off2  31844  ofresid  31845  xppreima2  31854  ofpreima2  31869  suppovss  31884  resf1o  31933  swrdrn3  32097  pwrssmgc  32148  mgcf1o  32151  gsumhashmul  32186  gsumle  32220  symgcom2  32223  pmtrcnel  32228  pmtrcnel2  32229  pmtrcnelor  32230  cycpmfvlem  32249  cycpmfv3  32252  cycpmcl  32253  cycpmco2rn  32262  cycpmco2  32270  cycpm3cl2  32273  cyc3co2  32277  cyc3evpm  32287  islinds5  32449  ellspds  32450  ghmquskerlem1  32491  ghmquskerco  32492  ghmqusker  32494  rhmpreimaidl  32499  elrspunidl  32504  elrspunsn  32505  rhmimaidl  32508  rhmpreimaprmidl  32528  evls1fn  32592  evls1fpws  32596  ressply1evl  32597  ply1degltel  32613  ply1degltlss  32614  ply1gsumz  32616  ply1degltdimlem  32652  ply1degltdim  32653  dimkerim  32657  fedgmullem2  32660  fedgmul  32661  irngss  32696  irngnzply1  32700  cmpcref  32768  rhmpreimacnlem  32802  fsumcvg4  32868  pl1cn  32873  qqhval2lem  32899  prodindf  32959  indpreima  32961  esumcvg  33022  ofcf  33039  ofcof  33043  measfn  33140  meascnbl  33155  sibfof  33277  sitgaddlemb  33285  subiwrdlen  33323  rrvfn  33382  plymul02  33495  signsplypnf  33499  signsply0  33500  reprsuc  33565  reprdifc  33577  breprexplema  33580  circlemethhgt  33593  hgt750lemb  33606  f1resrcmplf1dlem  34027  pthhashvtx  34056  cvmopnlem  34207  cvmliftmolem1  34210  cvmliftlem10  34223  cvmlift2lem9a  34232  cvmlift2lem6  34237  cvmlift2lem12  34243  cvmliftphtlem  34246  cvmlift3lem9  34256  mrsubrn  34442  elmrsubrn  34449  elmsubrn  34457  msubrn  34458  mclsind  34499  mclsppslem  34512  mclspps  34513  iprodefisumlem  34648  gg-dvmulbr  35113  matunitlindflem1  36422  poimirlem1  36427  poimirlem2  36428  poimirlem3  36429  poimirlem16  36442  poimirlem17  36443  poimirlem19  36445  poimirlem20  36446  poimirlem22  36448  poimirlem23  36449  poimirlem29  36455  poimirlem30  36456  poimirlem31  36457  poimir  36459  mblfinlem2  36464  itg2addnclem3  36479  itg2addnc  36480  itg2gt0cn  36481  ftc1cnnc  36498  ftc1anclem5  36503  ftc1anclem7  36505  ftc1anc  36507  sdclem2  36548  istotbnd3  36577  sstotbnd2  36580  isbnd3  36590  heibor1lem  36615  rrnmet  36635  grpokerinj  36699  isdrngo2  36764  lfl1  37878  lfladdcl  37879  lflvscl  37885  lkr0f  37902  lkrsc  37905  eqlkr2  37908  eqlkr3  37909  ldualvaddval  37939  ldualvsval  37946  tendoeq1  39573  sticksstones1  40900  sticksstones2  40901  sticksstones3  40902  sticksstones12a  40911  sticksstones12  40912  metakunt19  40941  metakunt25  40947  metakunt33  40955  frlmvscadiccat  41029  frlmsnic  41060  pwsgprod  41064  mplmapghm  41078  evlsvvval  41085  evlsaddval  41090  evlsmulval  41091  evladdval  41097  evlmulval  41098  selvvvval  41107  evlselvlem  41108  evlselv  41109  fsuppssind  41115  mhphf  41119  ismrcd1  41369  ismrcd2  41370  istopclsd  41371  isnacs3  41381  mzpaddmpt  41412  mzpmulmpt  41413  mzpsubst  41419  mzpcong  41644  fnwe2lem2  41726  islmodfg  41744  kercvrlsm  41758  dgrsub2  41810  mpaaeu  41825  rngunsnply  41848  idomrootle  41870  hausgraph  41887  ofoafg  42037  ofoafo  42039  ofoaid1  42041  ofoaid2  42042  naddcnff  42045  naddcnffn  42046  naddcnffo  42047  naddcnfcom  42049  naddcnfid1  42050  naddcnfass  42052  fsovf1od  42700  brcoffn  42714  clsneiel1  42792  wfximgfd  42848  extoimad  42849  mnringmulrcld  42920  mnurndlem1  42973  caofcan  43015  ofmul12  43017  ofdivrec  43018  ofdivcan4  43019  ofdivdiv2  43020  dvconstbi  43026  binomcxplemnotnn0  43048  refsum2cnlem1  43654  ssmapsn  43848  preimaiocmnf  44209  fsumsupp0  44229  fsumsermpt  44230  climinf  44257  climinf2lem  44357  limsupmnflem  44371  limsupvaluz2  44389  supcnvlimsup  44391  limsupgtlem  44428  liminfvalxr  44434  liminflelimsupuz  44436  xlimconst2  44486  climxlim2  44497  icccncfext  44538  dvnprodlem1  44597  volicoff  44646  voliooicof  44647  fourierdlem25  44783  etransclem2  44887  etransclem35  44920  fge0iccico  45021  sge0tsms  45031  sge0sup  45042  sge0resrn  45055  sge0le  45058  sge0fodjrnlem  45067  sge0isum  45078  sge0seq  45097  nnfoctbdjlem  45106  meadjiunlem  45116  omeiunle  45168  hoicvr  45199  ovolval4lem1  45300  ovolval5lem3  45305  ovnovollem1  45307  ovnovollem2  45308  iinhoiicclem  45324  iunhoiioolem  45326  preimaicomnf  45362  smfresal  45439  smfsuplem1  45462  smflimsuplem2  45472  fcoreslem3  45710  fcoreslem4  45711  fcores  45712  mgmhmf1o  46492  resmgmhm2b  46505  mgmhmima  46507  mgmhmeql  46508  prdsmulrngcl  46611  prdsrngd  46612  rnghmf1o  46635  rhmimasubrnglem  46677  ackvalsucsucval  47276  amgmwlem  47751