Theorem ffnd 6689

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

Syntax hints:   → wi 4   Fn wfn 6506  ⟶wf 6507

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 6515

This theorem is referenced by:  fnconstg  6748  f1fn  6757  fofn  6774  f1ofn  6801  feqmptd  6929  fssrescdmd  7098  fprb  7168  cocan1  7266  oprres  7557  off  7671  coof  7677  ofco  7678  caofref  7684  caofid0l  7686  caofid0r  7687  caofid1  7688  caofid2  7689  caofrss  7692  caoftrn  7694  fo2ndf  8100  fnwelem  8110  fnse  8112  suppsnop  8157  suppss  8173  suppssr  8174  suppssrg  8175  suppssof1  8178  suppofssd  8182  suppofss1d  8183  suppofss2d  8184  suppcoss  8186  smocdmdom  8337  elmapfn  8838  ralxpmap  8869  omxpenlem  9042  mapen  9105  f1finf1o  9216  f1finf1oOLD  9217  unirnffid  9298  fdmfifsupp  9326  mapfien  9359  intrnfi  9367  marypha2  9390  ordtypelem7  9477  wemapsolem  9503  wemapso  9504  wemapso2lem  9505  unxpwdom2  9541  ixpiunwdom  9543  cantnfle  9624  cantnfp1lem2  9632  cantnfp1lem3  9633  cantnfp1  9634  oemapvali  9637  cantnflem1a  9638  cantnflem1c  9640  cantnflem3  9644  cantnf  9646  cnfcomlem  9652  cnfcom3  9657  updjudhcoinlf  9885  updjudhcoinrg  9886  fseqenlem1  9977  numacn  10002  infpwfien  10015  isf32lem2  10307  isf34lem7  10332  isf34lem6  10333  unirnfdomd  10520  ofsubeq0  12183  ofnegsub  12184  ofsubge0  12185  seqf1olem2  14007  resunimafz0  14410  wrdfn  14493  swrdvalfn  14616  pfxfn  14646  pfxid  14649  cats1un  14686  cshwfn  14766  ccatco  14801  limsupgle  15443  o1of2  15579  o1rlimmul  15585  isercolllem2  15632  isercoll  15634  isercoll2  15635  climsup  15636  fsumss  15691  ruclem11  16208  vdwlem2  16953  vdwlem6  16957  vdwlem9  16960  vdwlem12  16963  0ram  16991  ramub1lem1  16997  pwsle  17455  pwsleval  17456  pwsvscaval  17458  mrcuni  17582  mrcun  17583  invf1o  17731  funcres2c  17865  setcmon  18049  setcepi  18050  uncfcurf  18200  yoniso  18246  isacs4lem  18503  acsmapd  18513  gsumval2  18613  mgmhmf1o  18627  resmgmhm2b  18640  mgmhmima  18642  mgmhmeql  18643  prdsplusgsgrpcl  18659  prdssgrpd  18660  prdsplusgcl  18695  prdsidlem  18696  prdsmndd  18697  mhmf1o  18723  resmhm2b  18749  mhmimalem  18751  mhmima  18752  mhmeql  18753  prdspjmhm  18756  pwsco1mhm  18759  pwsco2mhm  18760  gsumwmhm  18772  frmdss2  18790  grpinvf1o  18941  prdsinvlem  18981  cycsubgcl  19138  ghmrn  19161  ghmpreima  19170  ghmeql  19171  ghmnsgima  19172  ghmnsgpreima  19173  ghmeqker  19175  ghmf1o  19180  ghmqusnsglem1  19212  ghmqusnsg  19214  ghmquskerlem1  19215  ghmquskerco  19216  ghmquskerlem3  19218  ghmqusker  19219  gass  19233  cntzmhm  19273  symgextres  19355  gsmsymgrfixlem1  19357  fvcosymgeq  19359  f1omvdconj  19376  pmtrfinv  19391  symgtrinv  19402  pmtr3ncomlem1  19403  sygbasnfpfi  19442  efginvrel2  19657  efgredleme  19673  ghmplusg  19776  prdscmnd  19791  gsumval3a  19833  gsumval3eu  19834  gsumzaddlem  19851  gsumzsplit  19857  gsumpt  19892  prdsgsum  19911  dprdfcntz  19947  dprdfadd  19952  dprdfeq0  19954  dprdf11  19955  dprdlub  19958  dprdspan  19959  dprd2dlem1  19973  dmdprdpr  19981  dprdpr  19982  dpjlem  19983  ablfac1eu  20005  prdsmulrngcl  20084  prdsrngd  20085  prdsringd  20230  prdscrngd  20231  prds1  20232  pwspjmhmmgpd  20237  rnghmf1o  20361  rhmf1o  20400  rhmimasubrnglem  20474  rnrhmsubrg  20514  rrgsupp  20610  imadrhmcl  20706  isabvd  20721  lmodfopnelem1  20804  lcomfsupp  20808  prdsvscacl  20874  prdslmodd  20875  lmhmco  20950  lmhmplusg  20951  lmhmvsca  20952  lmhmf1o  20953  lmhmeql  20962  lspextmo  20963  rhmpreimaidl  21187  pjfo  21624  dsmmbas2  21646  dsmm0cl  21649  dsmmacl  21650  dsmmsubg  21652  dsmmlss  21653  frlmvplusgvalc  21676  frlmvscaval  21677  frlmplusgvalb  21678  frlmvscavalb  21679  frlmsslss2  21684  frlmphllem  21689  frlmphl  21690  frlmssuvc2  21704  frlmsslsp  21705  frlmup1  21707  frlmup2  21708  frlmup3  21709  frlmup4  21710  islindf4  21747  psrbagfsupp  21828  psrbaglesupp  21831  psrbaglecl  21832  psrbagaddcl  21833  psrbagcon  21834  psrbaglefi  21835  psrbagleadd1  21837  psrbagconf1o  21838  gsumbagdiaglem  21839  psrass1lem  21841  psrvscaval  21859  psrlidm  21871  psrridm  21872  psrass1  21873  psrdi  21874  psrdir  21875  psrascl  21888  mvrf2  21902  mplsubglem  21908  mplvscaval  21925  subrgmvrf  21941  mplbas2  21949  mplind  21977  psrbagev1  21984  psrbagev2  21985  evlslem3  21987  evlslem1  21989  evlsvar  21997  mpfind  22014  ismhp3  22029  mhpmulcl  22036  psdmplcl  22049  psdadd  22050  psdvsca  22051  psdmul  22053  psdmvr  22056  psrplusgpropd  22120  coe1add  22150  coe1addfv  22151  evl1addd  22228  evl1subd  22229  evl1muld  22230  pf1mpf  22239  pf1ind  22242  evls1fpws  22256  ressply1evl  22257  rhmply1vsca  22275  mamudir  22291  mamulid  22328  mamurid  22329  mdetrlin  22489  mdetrsca  22490  mdetralt  22495  mdetunilem7  22505  mdetunilem9  22507  madurid  22531  cnrest2  23173  lmss  23185  lmcnp  23191  cnt0  23233  cnt1  23237  cnhaus  23241  rncmp  23283  conncn  23313  2ndcomap  23345  1stccnp  23349  comppfsc  23419  1stckgenlem  23440  ptbasfi  23468  ptopn  23470  ptclsg  23502  ptcnp  23509  upxp  23510  txtube  23527  txcmplem1  23528  hauseqlcld  23533  xkohaus  23540  xkoptsub  23541  cnmpt11  23550  cnmpt21  23558  cnmpt22f  23562  cnmptcom  23565  qtopss  23602  qtopeu  23603  qtopomap  23605  qtopcmap  23606  kqffn  23612  hmeof1o2  23650  xkocnv  23701  rnelfm  23840  ptcmplem1  23939  cnextfres1  23955  ghmcnp  24002  tgphaus  24004  prdstmdd  24011  prdstgpd  24012  fmucnd  24179  psmetxrge0  24201  isxmet2d  24215  prdsmet  24258  blelrnps  24304  blelrn  24305  xmetresbl  24325  comet  24401  stdbdxmet  24403  met2ndci  24410  prdsxmslem2  24417  isngp3  24486  nmotri  24627  metdsre  24742  bndth  24857  evth  24858  fmcfil  25172  bcthlem4  25227  rrxcph  25292  rrxds  25293  rrxmet  25308  evthicc2  25361  ovolfsf  25372  ovolmge0  25378  ovollb2lem  25389  ovolunlem1a  25397  ovoliunlem1  25403  ovoliun  25406  ovoliun2  25407  ovolscalem1  25414  ovolicc1  25417  ovolicc2lem4  25421  ovolicc2  25423  voliunlem1  25451  voliunlem3  25453  volsup  25457  ioombl1lem2  25460  ioombl1lem4  25462  uniiccdif  25479  uniioombllem2  25484  uniioombllem3  25486  uniioombllem6  25489  volsup2  25506  vitalilem4  25512  mbfeqalem1  25542  mbfmulc2lem  25548  mbfmax  25550  mbfaddlem  25561  mbfadd  25562  mbfsub  25563  mbfsup  25565  mbfinf  25566  itg1ge0  25587  itg1addlem1  25593  i1faddlem  25594  i1fmullem  25595  i1fadd  25596  i1fmul  25597  itg1addlem4  25600  i1fmulclem  25603  i1fmulc  25604  itg1mulc  25605  i1fres  25606  itg10a  25611  itg1ge0a  25612  itg1lea  25613  mbfi1fseqlem3  25618  mbfi1fseqlem4  25619  mbfi1flimlem  25623  mbfmullem2  25625  mbfmul  25627  itg20  25638  itg2lea  25645  itg2splitlem  25649  itg2split  25650  itg2monolem1  25651  itg2monolem2  25652  itg2monolem3  25653  itg2mono  25654  itg2i1fseqle  25655  itg2i1fseq  25656  itg2addlem  25659  itg2gt0  25661  itg2cnlem1  25662  itg2cnlem2  25663  itg2cn  25664  itgitg1  25710  bddmulibl  25740  bddibl  25741  dvidlem  25816  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvaddf  25845  dvcmulf  25848  dvrec  25859  dvcnvlem  25880  rolle  25894  dveq0  25905  dv11cn  25906  dvivthlem2  25914  dvivth  25915  dvne0  25916  lhop1lem  25918  lhop1  25919  lhop2  25920  lhop  25921  ftc1cn  25950  tdeglem1  25963  tdeglem3  25964  tdeglem4  25965  mdegleb  25969  mdegldg  25971  mdegaddle  25979  ply1remlem  26070  ply1rem  26071  fta1glem1  26073  fta1glem2  26074  fta1blem  26076  idomrootle  26078  plyeq0lem  26115  plyeq0  26116  plyaddlem1  26118  coeeulem  26129  coeaddlem  26154  coemulc  26160  dgradd2  26174  dgrcolem2  26180  ofmulrt  26189  plyrem  26213  vieta1lem1  26218  vieta1  26220  plyexmo  26221  elqaalem3  26229  aannenlem1  26236  aalioulem2  26241  ulmuni  26301  ulmdvlem1  26309  ulmdv  26312  mbfulm  26315  iblulm  26316  itgulm  26317  rlimcnp2  26876  jensen  26899  amgm  26901  basellem3  26993  basellem7  26997  basellem9  26999  dchrelbas2  27148  dchrmulcl  27160  dchrfi  27166  dchreq  27169  dchrresb  27170  dchrinv  27172  dchr1re  27174  sumdchr2  27181  dchr2sum  27184  lgsqrlem2  27258  lgsqrlem3  27259  rpvmasum2  27423  dchrisum0re  27424  mirf1o  28596  lmif1o  28722  eqeefv  28830  axlowdimlem14  28882  vtxdgfisf  29404  2pthon3v  29873  nvinvfval  30569  sspg  30657  ssps  30659  sspmlem  30661  sspn  30665  lnon0  30727  ubthlem1  30799  pjfn  31638  kbpj  31885  kbass2  32046  elpjrn  32119  ofrn2  32564  off2  32565  ofresid  32566  xppreima2  32575  ofpreima2  32590  suppovss  32604  resf1o  32653  prodindf  32786  indpreima  32788  swrdrn3  32877  pwrssmgc  32926  mgcf1o  32929  chnso  32940  gsumfs2d  32995  gsumhashmul  33001  gsumle  33038  symgcom2  33041  pmtrcnel  33046  pmtrcnel2  33047  pmtrcnelor  33048  cycpmfvlem  33069  cycpmfv3  33072  cycpmcl  33073  cycpmco2rn  33082  cycpmco2  33090  cycpm3cl2  33093  cyc3co2  33097  cyc3evpm  33107  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem4  33196  elrgspnsubrunlem1  33198  elrgspnsubrunlem2  33199  islinds5  33338  ellspds  33339  elrspunidl  33399  elrspunsn  33400  rhmimaidl  33403  rhmpreimaprmidl  33422  rprmdvdsprod  33505  1arithidomlem2  33507  evls1fn  33529  ply1dg1rt  33548  ply1mulrtss  33550  ply1degltel  33560  ply1degleel  33561  ply1degltlss  33562  ply1gsumz  33564  ig1pmindeg  33567  r1pquslmic  33576  exsslsb  33592  ply1degltdimlem  33618  ply1degltdim  33619  dimkerim  33623  fedgmullem2  33626  fedgmul  33627  lvecendof1f1o  33629  fldextrspunlsplem  33668  fldextrspunlsp  33669  irngss  33682  irngnzply1  33686  irngnminplynz  33702  2sqr3minply  33770  cos9thpiminply  33778  cmpcref  33840  rhmpreimacnlem  33874  fsumcvg4  33940  pl1cn  33945  qqhval2lem  33971  esumcvg  34076  ofcf  34093  ofcof  34097  measfn  34194  meascnbl  34209  sibfof  34331  sitgaddlemb  34339  subiwrdlen  34377  rrvfn  34436  plymul02  34537  signsplypnf  34541  signsply0  34542  reprsuc  34606  reprdifc  34618  breprexplema  34621  circlemethhgt  34634  hgt750lemb  34647  f1resrcmplf1dlem  35076  pthhashvtx  35115  cvmopnlem  35265  cvmliftmolem1  35268  cvmliftlem10  35281  cvmlift2lem9a  35290  cvmlift2lem6  35295  cvmlift2lem12  35301  cvmliftphtlem  35304  cvmlift3lem9  35314  mrsubrn  35500  elmrsubrn  35507  elmsubrn  35515  msubrn  35516  mclsind  35557  mclsppslem  35570  mclspps  35571  iprodefisumlem  35727  weiunfrlem  36452  matunitlindflem1  37610  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem22  37636  poimirlem23  37637  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  poimir  37647  mblfinlem2  37652  itg2addnclem3  37667  itg2addnc  37668  itg2gt0cn  37669  ftc1cnnc  37686  ftc1anclem5  37691  ftc1anclem7  37693  ftc1anc  37695  sdclem2  37736  istotbnd3  37765  sstotbnd2  37768  isbnd3  37778  heibor1lem  37803  rrnmet  37823  grpokerinj  37887  isdrngo2  37952  lfl1  39063  lfladdcl  39064  lflvscl  39070  lkr0f  39087  lkrsc  39090  eqlkr2  39093  eqlkr3  39094  ldualvaddval  39124  ldualvsval  39131  tendoeq1  40758  zndvdchrrhm  41960  hashscontpow  42110  aks6d1c3  42111  aks6d1c2lem4  42115  aks6d1c2  42118  sticksstones1  42134  sticksstones2  42135  sticksstones3  42136  sticksstones12a  42145  sticksstones12  42146  aks6d1c6lem2  42159  aks6d1c6lem3  42160  aks6d1c6isolem1  42162  aks6d1c6isolem3  42164  aks6d1c6lem5  42165  aks6d1c7lem1  42168  unitscyglem1  42183  dvun  42347  frlmvscadiccat  42494  fiabv  42524  frlmsnic  42528  pwsgprod  42532  mplmapghm  42544  evlsvvval  42551  evlsaddval  42556  evlsmulval  42557  evladdval  42563  evlmulval  42564  selvvvval  42573  evlselvlem  42574  evlselv  42575  fsuppssind  42581  mhphf  42585  ismrcd1  42686  ismrcd2  42687  istopclsd  42688  isnacs3  42698  mzpaddmpt  42729  mzpmulmpt  42730  mzpsubst  42736  mzpcong  42961  fnwe2lem2  43040  islmodfg  43058  kercvrlsm  43072  dgrsub2  43124  mpaaeu  43139  rngunsnply  43158  hausgraph  43194  ofoafg  43343  ofoafo  43345  ofoaid1  43347  ofoaid2  43348  naddcnff  43351  naddcnffn  43352  naddcnffo  43353  naddcnfcom  43355  naddcnfid1  43356  naddcnfass  43358  fsovf1od  44005  brcoffn  44019  clsneiel1  44097  wfximgfd  44152  extoimad  44153  mnringmulrcld  44217  mnurndlem1  44270  caofcan  44312  ofmul12  44314  ofdivrec  44315  ofdivcan4  44316  ofdivdiv2  44317  dvconstbi  44323  binomcxplemnotnn0  44345  relpmin  44942  refsum2cnlem1  45031  ssmapsn  45210  preimaiocmnf  45558  fsumsupp0  45576  fsumsermpt  45577  climinf  45604  climinf2lem  45704  limsupmnflem  45718  limsupvaluz2  45736  supcnvlimsup  45738  limsupgtlem  45775  liminfvalxr  45781  liminflelimsupuz  45783  xlimconst2  45833  climxlim2  45844  icccncfext  45885  dvnprodlem1  45944  volicoff  45993  voliooicof  45994  fourierdlem25  46130  etransclem2  46234  etransclem35  46267  fge0iccico  46368  sge0tsms  46378  sge0sup  46389  sge0resrn  46402  sge0le  46405  sge0fodjrnlem  46414  sge0isum  46425  sge0seq  46444  nnfoctbdjlem  46453  meadjiunlem  46463  omeiunle  46515  hoicvr  46546  ovolval4lem1  46647  ovolval5lem3  46652  ovnovollem1  46654  ovnovollem2  46655  iinhoiicclem  46671  iunhoiioolem  46673  preimaicomnf  46709  smfresal  46786  smfsuplem1  46809  smflimsuplem2  46819  fcoreslem3  47066  fcoreslem4  47067  fcores  47068  isubgredg  47866  upgrimpths  47909  ackvalsucsucval  48677  funchomf  49086  imasubc  49140  imassc  49142  imaid  49143  prcofdiag1  49382  prcofdiag  49383  oppfdiag1  49403  oppfdiag  49405  amgmwlem  49791