Theorem ffnd 6703

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

Syntax hints:   → wi 4   Fn wfn 6522  ⟶wf 6523

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 207  df-an 396  df-f 6531

This theorem is referenced by:  fnconstg  6762  f1fn  6771  fofn  6788  f1ofn  6815  feqmptd  6943  fssrescdmd  7112  fprb  7182  cocan1  7279  oprres  7569  off  7683  coof  7689  ofco  7690  caofref  7696  caofid0l  7698  caofid0r  7699  caofid1  7700  caofid2  7701  caofrss  7704  caoftrn  7706  fo2ndf  8114  fnwelem  8124  fnse  8126  suppsnop  8171  suppss  8187  suppssr  8188  suppssrg  8189  suppssof1  8192  suppofssd  8196  suppofss1d  8197  suppofss2d  8198  suppcoss  8200  smocdmdom  8376  elmapfn  8873  ralxpmap  8904  omxpenlem  9081  mapen  9149  f1finf1o  9271  f1finf1oOLD  9272  unirnffid  9353  fdmfifsupp  9381  mapfien  9414  intrnfi  9422  marypha2  9445  ordtypelem7  9530  wemapsolem  9556  wemapso  9557  wemapso2lem  9558  unxpwdom2  9594  ixpiunwdom  9596  cantnfle  9677  cantnfp1lem2  9685  cantnfp1lem3  9686  cantnfp1  9687  oemapvali  9690  cantnflem1a  9691  cantnflem1c  9693  cantnflem3  9697  cantnf  9699  cnfcomlem  9705  cnfcom3  9710  updjudhcoinlf  9938  updjudhcoinrg  9939  fseqenlem1  10030  numacn  10055  infpwfien  10068  isf32lem2  10360  isf34lem7  10385  isf34lem6  10386  unirnfdomd  10573  ofsubeq0  12229  ofnegsub  12230  ofsubge0  12231  seqf1olem2  14049  resunimafz0  14451  wrdfn  14533  swrdvalfn  14656  pfxfn  14686  pfxid  14689  cats1un  14726  cshwfn  14806  ccatco  14841  limsupgle  15480  o1of2  15616  o1rlimmul  15622  isercolllem2  15669  isercoll  15671  isercoll2  15672  climsup  15673  fsumss  15728  ruclem11  16243  vdwlem2  16987  vdwlem6  16991  vdwlem9  16994  vdwlem12  16997  0ram  17025  ramub1lem1  17031  pwsle  17491  pwsleval  17492  pwsvscaval  17494  mrcuni  17618  mrcun  17619  invf1o  17767  funcres2c  17901  setcmon  18085  setcepi  18086  uncfcurf  18236  yoniso  18282  isacs4lem  18539  acsmapd  18549  gsumval2  18649  mgmhmf1o  18663  resmgmhm2b  18676  mgmhmima  18678  mgmhmeql  18679  prdsplusgsgrpcl  18695  prdssgrpd  18696  prdsplusgcl  18731  prdsidlem  18732  prdsmndd  18733  mhmf1o  18759  resmhm2b  18785  mhmimalem  18787  mhmima  18788  mhmeql  18789  prdspjmhm  18792  pwsco1mhm  18795  pwsco2mhm  18796  gsumwmhm  18808  frmdss2  18826  grpinvf1o  18977  prdsinvlem  19017  cycsubgcl  19174  ghmrn  19197  ghmpreima  19206  ghmeql  19207  ghmnsgima  19208  ghmnsgpreima  19209  ghmeqker  19211  ghmf1o  19216  ghmqusnsglem1  19248  ghmqusnsg  19250  ghmquskerlem1  19251  ghmquskerco  19252  ghmquskerlem3  19254  ghmqusker  19255  gass  19269  cntzmhm  19309  symgextres  19391  gsmsymgrfixlem1  19393  fvcosymgeq  19395  f1omvdconj  19412  pmtrfinv  19427  symgtrinv  19438  pmtr3ncomlem1  19439  sygbasnfpfi  19478  efginvrel2  19693  efgredleme  19709  ghmplusg  19812  prdscmnd  19827  gsumval3a  19869  gsumval3eu  19870  gsumzaddlem  19887  gsumzsplit  19893  gsumpt  19928  prdsgsum  19947  dprdfcntz  19983  dprdfadd  19988  dprdfeq0  19990  dprdf11  19991  dprdlub  19994  dprdspan  19995  dprd2dlem1  20009  dmdprdpr  20017  dprdpr  20018  dpjlem  20019  ablfac1eu  20041  prdsmulrngcl  20120  prdsrngd  20121  prdsringd  20266  prdscrngd  20267  prds1  20268  pwspjmhmmgpd  20273  rnghmf1o  20397  rhmf1o  20436  rhmimasubrnglem  20510  rnrhmsubrg  20550  rrgsupp  20646  imadrhmcl  20742  isabvd  20757  lmodfopnelem1  20840  lcomfsupp  20844  prdsvscacl  20910  prdslmodd  20911  lmhmco  20986  lmhmplusg  20987  lmhmvsca  20988  lmhmf1o  20989  lmhmeql  20998  lspextmo  20999  rhmpreimaidl  21223  pjfo  21660  dsmmbas2  21682  dsmm0cl  21685  dsmmacl  21686  dsmmsubg  21688  dsmmlss  21689  frlmvplusgvalc  21712  frlmvscaval  21713  frlmplusgvalb  21714  frlmvscavalb  21715  frlmsslss2  21720  frlmphllem  21725  frlmphl  21726  frlmssuvc2  21740  frlmsslsp  21741  frlmup1  21743  frlmup2  21744  frlmup3  21745  frlmup4  21746  islindf4  21783  psrbagfsupp  21864  psrbaglesupp  21867  psrbaglecl  21868  psrbagaddcl  21869  psrbagcon  21870  psrbaglefi  21871  psrbagleadd1  21873  psrbagconf1o  21874  gsumbagdiaglem  21875  psrass1lem  21877  psrvscaval  21895  psrlidm  21907  psrridm  21908  psrass1  21909  psrdi  21910  psrdir  21911  psrascl  21924  mvrf2  21938  mplsubglem  21944  mplvscaval  21961  subrgmvrf  21977  mplbas2  21985  mplind  22013  psrbagev1  22020  psrbagev2  22021  evlslem3  22023  evlslem1  22025  evlsvar  22033  mpfind  22050  ismhp3  22065  mhpmulcl  22072  psdmplcl  22085  psdadd  22086  psdvsca  22087  psdmul  22089  psdmvr  22092  psrplusgpropd  22156  coe1add  22186  coe1addfv  22187  evl1addd  22264  evl1subd  22265  evl1muld  22266  pf1mpf  22275  pf1ind  22278  evls1fpws  22292  ressply1evl  22293  rhmply1vsca  22311  mamudir  22327  mamulid  22364  mamurid  22365  mdetrlin  22525  mdetrsca  22526  mdetralt  22531  mdetunilem7  22541  mdetunilem9  22543  madurid  22567  cnrest2  23209  lmss  23221  lmcnp  23227  cnt0  23269  cnt1  23273  cnhaus  23277  rncmp  23319  conncn  23349  2ndcomap  23381  1stccnp  23385  comppfsc  23455  1stckgenlem  23476  ptbasfi  23504  ptopn  23506  ptclsg  23538  ptcnp  23545  upxp  23546  txtube  23563  txcmplem1  23564  hauseqlcld  23569  xkohaus  23576  xkoptsub  23577  cnmpt11  23586  cnmpt21  23594  cnmpt22f  23598  cnmptcom  23601  qtopss  23638  qtopeu  23639  qtopomap  23641  qtopcmap  23642  kqffn  23648  hmeof1o2  23686  xkocnv  23737  rnelfm  23876  ptcmplem1  23975  cnextfres1  23991  ghmcnp  24038  tgphaus  24040  prdstmdd  24047  prdstgpd  24048  fmucnd  24215  psmetxrge0  24237  isxmet2d  24251  prdsmet  24294  blelrnps  24340  blelrn  24341  xmetresbl  24361  comet  24437  stdbdxmet  24439  met2ndci  24446  prdsxmslem2  24453  isngp3  24522  nmotri  24663  metdsre  24778  bndth  24893  evth  24894  fmcfil  25209  bcthlem4  25264  rrxcph  25329  rrxds  25330  rrxmet  25345  evthicc2  25398  ovolfsf  25409  ovolmge0  25415  ovollb2lem  25426  ovolunlem1a  25434  ovoliunlem1  25440  ovoliun  25443  ovoliun2  25444  ovolscalem1  25451  ovolicc1  25454  ovolicc2lem4  25458  ovolicc2  25460  voliunlem1  25488  voliunlem3  25490  volsup  25494  ioombl1lem2  25497  ioombl1lem4  25499  uniiccdif  25516  uniioombllem2  25521  uniioombllem3  25523  uniioombllem6  25526  volsup2  25543  vitalilem4  25549  mbfeqalem1  25579  mbfmulc2lem  25585  mbfmax  25587  mbfaddlem  25598  mbfadd  25599  mbfsub  25600  mbfsup  25602  mbfinf  25603  itg1ge0  25624  itg1addlem1  25630  i1faddlem  25631  i1fmullem  25632  i1fadd  25633  i1fmul  25634  itg1addlem4  25637  i1fmulclem  25640  i1fmulc  25641  itg1mulc  25642  i1fres  25643  itg10a  25648  itg1ge0a  25649  itg1lea  25650  mbfi1fseqlem3  25655  mbfi1fseqlem4  25656  mbfi1flimlem  25660  mbfmullem2  25662  mbfmul  25664  itg20  25675  itg2lea  25682  itg2splitlem  25686  itg2split  25687  itg2monolem1  25688  itg2monolem2  25689  itg2monolem3  25690  itg2mono  25691  itg2i1fseqle  25692  itg2i1fseq  25693  itg2addlem  25696  itg2gt0  25698  itg2cnlem1  25699  itg2cnlem2  25700  itg2cn  25701  itgitg1  25747  bddmulibl  25777  bddibl  25778  dvidlem  25853  dvaddbr  25877  dvmulbr  25878  dvmulbrOLD  25879  dvaddf  25882  dvcmulf  25885  dvrec  25896  dvcnvlem  25917  rolle  25931  dveq0  25942  dv11cn  25943  dvivthlem2  25951  dvivth  25952  dvne0  25953  lhop1lem  25955  lhop1  25956  lhop2  25957  lhop  25958  ftc1cn  25987  tdeglem1  26000  tdeglem3  26001  tdeglem4  26002  mdegleb  26006  mdegldg  26008  mdegaddle  26016  ply1remlem  26107  ply1rem  26108  fta1glem1  26110  fta1glem2  26111  fta1blem  26113  idomrootle  26115  plyeq0lem  26152  plyeq0  26153  plyaddlem1  26155  coeeulem  26166  coeaddlem  26191  coemulc  26197  dgradd2  26211  dgrcolem2  26217  ofmulrt  26226  plyrem  26250  vieta1lem1  26255  vieta1  26257  plyexmo  26258  elqaalem3  26266  aannenlem1  26273  aalioulem2  26278  ulmuni  26338  ulmdvlem1  26346  ulmdv  26349  mbfulm  26352  iblulm  26353  itgulm  26354  rlimcnp2  26912  jensen  26935  amgm  26937  basellem3  27029  basellem7  27033  basellem9  27035  dchrelbas2  27184  dchrmulcl  27196  dchrfi  27202  dchreq  27205  dchrresb  27206  dchrinv  27208  dchr1re  27210  sumdchr2  27217  dchr2sum  27220  lgsqrlem2  27294  lgsqrlem3  27295  rpvmasum2  27459  dchrisum0re  27460  mirf1o  28580  lmif1o  28706  eqeefv  28814  axlowdimlem14  28866  vtxdgfisf  29388  2pthon3v  29857  nvinvfval  30553  sspg  30641  ssps  30643  sspmlem  30645  sspn  30649  lnon0  30711  ubthlem1  30783  pjfn  31622  kbpj  31869  kbass2  32030  elpjrn  32103  ofrn2  32551  off2  32552  ofresid  32553  xppreima2  32562  ofpreima2  32577  suppovss  32591  resf1o  32642  prodindf  32758  indpreima  32760  swrdrn3  32850  pwrssmgc  32899  mgcf1o  32902  chnso  32913  gsumfs2d  32967  gsumhashmul  32973  gsumle  33010  symgcom2  33013  pmtrcnel  33018  pmtrcnel2  33019  pmtrcnelor  33020  cycpmfvlem  33041  cycpmfv3  33044  cycpmcl  33045  cycpmco2rn  33054  cycpmco2  33062  cycpm3cl2  33065  cyc3co2  33069  cyc3evpm  33079  elrgspnlem1  33155  elrgspnlem2  33156  elrgspnlem4  33158  elrgspnsubrunlem1  33160  elrgspnsubrunlem2  33161  islinds5  33300  ellspds  33301  elrspunidl  33361  elrspunsn  33362  rhmimaidl  33365  rhmpreimaprmidl  33384  rprmdvdsprod  33467  1arithidomlem2  33469  evls1fn  33491  ply1dg1rt  33509  ply1mulrtss  33511  ply1degltel  33520  ply1degleel  33521  ply1degltlss  33522  ply1gsumz  33524  ig1pmindeg  33527  r1pquslmic  33536  exsslsb  33552  ply1degltdimlem  33578  ply1degltdim  33579  dimkerim  33583  fedgmullem2  33586  fedgmul  33587  lvecendof1f1o  33589  fldextrspunlsplem  33630  fldextrspunlsp  33631  irngss  33644  irngnzply1  33648  irngnminplynz  33662  2sqr3minply  33730  cmpcref  33789  rhmpreimacnlem  33823  fsumcvg4  33889  pl1cn  33894  qqhval2lem  33920  esumcvg  34025  ofcf  34042  ofcof  34046  measfn  34143  meascnbl  34158  sibfof  34280  sitgaddlemb  34288  subiwrdlen  34326  rrvfn  34385  plymul02  34499  signsplypnf  34503  signsply0  34504  reprsuc  34568  reprdifc  34580  breprexplema  34583  circlemethhgt  34596  hgt750lemb  34609  f1resrcmplf1dlem  35038  pthhashvtx  35071  cvmopnlem  35221  cvmliftmolem1  35224  cvmliftlem10  35237  cvmlift2lem9a  35246  cvmlift2lem6  35251  cvmlift2lem12  35257  cvmliftphtlem  35260  cvmlift3lem9  35270  mrsubrn  35456  elmrsubrn  35463  elmsubrn  35471  msubrn  35472  mclsind  35513  mclsppslem  35526  mclspps  35527  iprodefisumlem  35678  weiunfrlem  36403  matunitlindflem1  37561  poimirlem1  37566  poimirlem2  37567  poimirlem3  37568  poimirlem16  37581  poimirlem17  37582  poimirlem19  37584  poimirlem20  37585  poimirlem22  37587  poimirlem23  37588  poimirlem29  37594  poimirlem30  37595  poimirlem31  37596  poimir  37598  mblfinlem2  37603  itg2addnclem3  37618  itg2addnc  37619  itg2gt0cn  37620  ftc1cnnc  37637  ftc1anclem5  37642  ftc1anclem7  37644  ftc1anc  37646  sdclem2  37687  istotbnd3  37716  sstotbnd2  37719  isbnd3  37729  heibor1lem  37754  rrnmet  37774  grpokerinj  37838  isdrngo2  37903  lfl1  39009  lfladdcl  39010  lflvscl  39016  lkr0f  39033  lkrsc  39036  eqlkr2  39039  eqlkr3  39040  ldualvaddval  39070  ldualvsval  39077  tendoeq1  40704  zndvdchrrhm  41906  hashscontpow  42057  aks6d1c3  42058  aks6d1c2lem4  42062  aks6d1c2  42065  sticksstones1  42081  sticksstones2  42082  sticksstones3  42083  sticksstones12a  42092  sticksstones12  42093  aks6d1c6lem2  42106  aks6d1c6lem3  42107  aks6d1c6isolem1  42109  aks6d1c6isolem3  42111  aks6d1c6lem5  42112  aks6d1c7lem1  42115  unitscyglem1  42130  metakunt19  42158  metakunt25  42164  metakunt33  42172  dvun  42327  frlmvscadiccat  42454  fiabv  42484  frlmsnic  42488  pwsgprod  42492  mplmapghm  42504  evlsvvval  42511  evlsaddval  42516  evlsmulval  42517  evladdval  42523  evlmulval  42524  selvvvval  42533  evlselvlem  42534  evlselv  42535  fsuppssind  42541  mhphf  42545  ismrcd1  42646  ismrcd2  42647  istopclsd  42648  isnacs3  42658  mzpaddmpt  42689  mzpmulmpt  42690  mzpsubst  42696  mzpcong  42921  fnwe2lem2  43000  islmodfg  43018  kercvrlsm  43032  dgrsub2  43084  mpaaeu  43099  rngunsnply  43118  hausgraph  43154  ofoafg  43303  ofoafo  43305  ofoaid1  43307  ofoaid2  43308  naddcnff  43311  naddcnffn  43312  naddcnffo  43313  naddcnfcom  43315  naddcnfid1  43316  naddcnfass  43318  fsovf1od  43965  brcoffn  43979  clsneiel1  44057  wfximgfd  44112  extoimad  44113  mnringmulrcld  44178  mnurndlem1  44231  caofcan  44273  ofmul12  44275  ofdivrec  44276  ofdivcan4  44277  ofdivdiv2  44278  dvconstbi  44284  binomcxplemnotnn0  44306  relpmin  44904  refsum2cnlem1  44988  ssmapsn  45167  preimaiocmnf  45518  fsumsupp0  45537  fsumsermpt  45538  climinf  45565  climinf2lem  45665  limsupmnflem  45679  limsupvaluz2  45697  supcnvlimsup  45699  limsupgtlem  45736  liminfvalxr  45742  liminflelimsupuz  45744  xlimconst2  45794  climxlim2  45805  icccncfext  45846  dvnprodlem1  45905  volicoff  45954  voliooicof  45955  fourierdlem25  46091  etransclem2  46195  etransclem35  46228  fge0iccico  46329  sge0tsms  46339  sge0sup  46350  sge0resrn  46363  sge0le  46366  sge0fodjrnlem  46375  sge0isum  46386  sge0seq  46405  nnfoctbdjlem  46414  meadjiunlem  46424  omeiunle  46476  hoicvr  46507  ovolval4lem1  46608  ovolval5lem3  46613  ovnovollem1  46615  ovnovollem2  46616  iinhoiicclem  46632  iunhoiioolem  46634  preimaicomnf  46670  smfresal  46747  smfsuplem1  46770  smflimsuplem2  46780  fcoreslem3  47022  fcoreslem4  47023  fcores  47024  isubgredg  47797  ackvalsucsucval  48554  amgmwlem  49386