Theorem ffnd 6657

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

Syntax hints:   → wi 4   Fn wfn 6481  ⟶wf 6482

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 6490

This theorem is referenced by:  fnconstg  6716  f1fn  6725  fofn  6742  f1ofn  6769  feqmptd  6895  fssrescdmd  7064  fprb  7134  cocan1  7232  oprres  7521  off  7635  coof  7641  ofco  7642  caofref  7648  caofid0l  7650  caofid0r  7651  caofid1  7652  caofid2  7653  caofrss  7656  caoftrn  7658  fo2ndf  8061  fnwelem  8071  fnse  8073  suppsnop  8118  suppss  8134  suppssr  8135  suppssrg  8136  suppssof1  8139  suppofssd  8143  suppofss1d  8144  suppofss2d  8145  suppcoss  8147  smocdmdom  8298  elmapfn  8799  ralxpmap  8830  omxpenlem  9002  mapen  9065  f1finf1o  9174  f1finf1oOLD  9175  unirnffid  9256  fdmfifsupp  9284  mapfien  9317  intrnfi  9325  marypha2  9348  ordtypelem7  9435  wemapsolem  9461  wemapso  9462  wemapso2lem  9463  unxpwdom2  9499  ixpiunwdom  9501  cantnfle  9586  cantnfp1lem2  9594  cantnfp1lem3  9595  cantnfp1  9596  oemapvali  9599  cantnflem1a  9600  cantnflem1c  9602  cantnflem3  9606  cantnf  9608  cnfcomlem  9614  cnfcom3  9619  updjudhcoinlf  9847  updjudhcoinrg  9848  fseqenlem1  9937  numacn  9962  infpwfien  9975  isf32lem2  10267  isf34lem7  10292  isf34lem6  10293  unirnfdomd  10480  ofsubeq0  12143  ofnegsub  12144  ofsubge0  12145  seqf1olem2  13967  resunimafz0  14370  wrdfn  14453  swrdvalfn  14576  pfxfn  14606  pfxid  14609  cats1un  14645  cshwfn  14725  ccatco  14760  limsupgle  15402  o1of2  15538  o1rlimmul  15544  isercolllem2  15591  isercoll  15593  isercoll2  15594  climsup  15595  fsumss  15650  ruclem11  16167  vdwlem2  16912  vdwlem6  16916  vdwlem9  16919  vdwlem12  16922  0ram  16950  ramub1lem1  16956  pwsle  17414  pwsleval  17415  pwsvscaval  17417  mrcuni  17545  mrcun  17546  invf1o  17694  funcres2c  17828  setcmon  18012  setcepi  18013  uncfcurf  18163  yoniso  18209  isacs4lem  18468  acsmapd  18478  gsumval2  18578  mgmhmf1o  18592  resmgmhm2b  18605  mgmhmima  18607  mgmhmeql  18608  prdsplusgsgrpcl  18624  prdssgrpd  18625  prdsplusgcl  18660  prdsidlem  18661  prdsmndd  18662  mhmf1o  18688  resmhm2b  18714  mhmimalem  18716  mhmima  18717  mhmeql  18718  prdspjmhm  18721  pwsco1mhm  18724  pwsco2mhm  18725  gsumwmhm  18737  frmdss2  18755  grpinvf1o  18906  prdsinvlem  18946  cycsubgcl  19103  ghmrn  19126  ghmpreima  19135  ghmeql  19136  ghmnsgima  19137  ghmnsgpreima  19138  ghmeqker  19140  ghmf1o  19145  ghmqusnsglem1  19177  ghmqusnsg  19179  ghmquskerlem1  19180  ghmquskerco  19181  ghmquskerlem3  19183  ghmqusker  19184  gass  19198  cntzmhm  19238  symgextres  19322  gsmsymgrfixlem1  19324  fvcosymgeq  19326  f1omvdconj  19343  pmtrfinv  19358  symgtrinv  19369  pmtr3ncomlem1  19370  sygbasnfpfi  19409  efginvrel2  19624  efgredleme  19640  ghmplusg  19743  prdscmnd  19758  gsumval3a  19800  gsumval3eu  19801  gsumzaddlem  19818  gsumzsplit  19824  gsumpt  19859  prdsgsum  19878  dprdfcntz  19914  dprdfadd  19919  dprdfeq0  19921  dprdf11  19922  dprdlub  19925  dprdspan  19926  dprd2dlem1  19940  dmdprdpr  19948  dprdpr  19949  dpjlem  19950  ablfac1eu  19972  gsumle  20042  prdsmulrngcl  20078  prdsrngd  20079  prdsringd  20224  prdscrngd  20225  prds1  20226  pwspjmhmmgpd  20231  rnghmf1o  20355  rhmf1o  20394  rhmimasubrnglem  20468  rnrhmsubrg  20508  rrgsupp  20604  imadrhmcl  20700  isabvd  20715  lmodfopnelem1  20819  lcomfsupp  20823  prdsvscacl  20889  prdslmodd  20890  lmhmco  20965  lmhmplusg  20966  lmhmvsca  20967  lmhmf1o  20968  lmhmeql  20977  lspextmo  20978  rhmpreimaidl  21202  pjfo  21640  dsmmbas2  21662  dsmm0cl  21665  dsmmacl  21666  dsmmsubg  21668  dsmmlss  21669  frlmvplusgvalc  21692  frlmvscaval  21693  frlmplusgvalb  21694  frlmvscavalb  21695  frlmsslss2  21700  frlmphllem  21705  frlmphl  21706  frlmssuvc2  21720  frlmsslsp  21721  frlmup1  21723  frlmup2  21724  frlmup3  21725  frlmup4  21726  islindf4  21763  psrbagfsupp  21844  psrbaglesupp  21847  psrbaglecl  21848  psrbagaddcl  21849  psrbagcon  21850  psrbaglefi  21851  psrbagleadd1  21853  psrbagconf1o  21854  gsumbagdiaglem  21855  psrass1lem  21857  psrvscaval  21875  psrlidm  21887  psrridm  21888  psrass1  21889  psrdi  21890  psrdir  21891  psrascl  21904  mvrf2  21918  mplsubglem  21924  mplvscaval  21941  subrgmvrf  21957  mplbas2  21965  mplind  21993  psrbagev1  22000  psrbagev2  22001  evlslem3  22003  evlslem1  22005  evlsvar  22013  mpfind  22030  ismhp3  22045  mhpmulcl  22052  psdmplcl  22065  psdadd  22066  psdvsca  22067  psdmul  22069  psdmvr  22072  psrplusgpropd  22136  coe1add  22166  coe1addfv  22167  evl1addd  22244  evl1subd  22245  evl1muld  22246  pf1mpf  22255  pf1ind  22258  evls1fpws  22272  ressply1evl  22273  rhmply1vsca  22291  mamudir  22307  mamulid  22344  mamurid  22345  mdetrlin  22505  mdetrsca  22506  mdetralt  22511  mdetunilem7  22521  mdetunilem9  22523  madurid  22547  cnrest2  23189  lmss  23201  lmcnp  23207  cnt0  23249  cnt1  23253  cnhaus  23257  rncmp  23299  conncn  23329  2ndcomap  23361  1stccnp  23365  comppfsc  23435  1stckgenlem  23456  ptbasfi  23484  ptopn  23486  ptclsg  23518  ptcnp  23525  upxp  23526  txtube  23543  txcmplem1  23544  hauseqlcld  23549  xkohaus  23556  xkoptsub  23557  cnmpt11  23566  cnmpt21  23574  cnmpt22f  23578  cnmptcom  23581  qtopss  23618  qtopeu  23619  qtopomap  23621  qtopcmap  23622  kqffn  23628  hmeof1o2  23666  xkocnv  23717  rnelfm  23856  ptcmplem1  23955  cnextfres1  23971  ghmcnp  24018  tgphaus  24020  prdstmdd  24027  prdstgpd  24028  fmucnd  24195  psmetxrge0  24217  isxmet2d  24231  prdsmet  24274  blelrnps  24320  blelrn  24321  xmetresbl  24341  comet  24417  stdbdxmet  24419  met2ndci  24426  prdsxmslem2  24433  isngp3  24502  nmotri  24643  metdsre  24758  bndth  24873  evth  24874  fmcfil  25188  bcthlem4  25243  rrxcph  25308  rrxds  25309  rrxmet  25324  evthicc2  25377  ovolfsf  25388  ovolmge0  25394  ovollb2lem  25405  ovolunlem1a  25413  ovoliunlem1  25419  ovoliun  25422  ovoliun2  25423  ovolscalem1  25430  ovolicc1  25433  ovolicc2lem4  25437  ovolicc2  25439  voliunlem1  25467  voliunlem3  25469  volsup  25473  ioombl1lem2  25476  ioombl1lem4  25478  uniiccdif  25495  uniioombllem2  25500  uniioombllem3  25502  uniioombllem6  25505  volsup2  25522  vitalilem4  25528  mbfeqalem1  25558  mbfmulc2lem  25564  mbfmax  25566  mbfaddlem  25577  mbfadd  25578  mbfsub  25579  mbfsup  25581  mbfinf  25582  itg1ge0  25603  itg1addlem1  25609  i1faddlem  25610  i1fmullem  25611  i1fadd  25612  i1fmul  25613  itg1addlem4  25616  i1fmulclem  25619  i1fmulc  25620  itg1mulc  25621  i1fres  25622  itg10a  25627  itg1ge0a  25628  itg1lea  25629  mbfi1fseqlem3  25634  mbfi1fseqlem4  25635  mbfi1flimlem  25639  mbfmullem2  25641  mbfmul  25643  itg20  25654  itg2lea  25661  itg2splitlem  25665  itg2split  25666  itg2monolem1  25667  itg2monolem2  25668  itg2monolem3  25669  itg2mono  25670  itg2i1fseqle  25671  itg2i1fseq  25672  itg2addlem  25675  itg2gt0  25677  itg2cnlem1  25678  itg2cnlem2  25679  itg2cn  25680  itgitg1  25726  bddmulibl  25756  bddibl  25757  dvidlem  25832  dvaddbr  25856  dvmulbr  25857  dvmulbrOLD  25858  dvaddf  25861  dvcmulf  25864  dvrec  25875  dvcnvlem  25896  rolle  25910  dveq0  25921  dv11cn  25922  dvivthlem2  25930  dvivth  25931  dvne0  25932  lhop1lem  25934  lhop1  25935  lhop2  25936  lhop  25937  ftc1cn  25966  tdeglem1  25979  tdeglem3  25980  tdeglem4  25981  mdegleb  25985  mdegldg  25987  mdegaddle  25995  ply1remlem  26086  ply1rem  26087  fta1glem1  26089  fta1glem2  26090  fta1blem  26092  idomrootle  26094  plyeq0lem  26131  plyeq0  26132  plyaddlem1  26134  coeeulem  26145  coeaddlem  26170  coemulc  26176  dgradd2  26190  dgrcolem2  26196  ofmulrt  26205  plyrem  26229  vieta1lem1  26234  vieta1  26236  plyexmo  26237  elqaalem3  26245  aannenlem1  26252  aalioulem2  26257  ulmuni  26317  ulmdvlem1  26325  ulmdv  26328  mbfulm  26331  iblulm  26332  itgulm  26333  rlimcnp2  26892  jensen  26915  amgm  26917  basellem3  27009  basellem7  27013  basellem9  27015  dchrelbas2  27164  dchrmulcl  27176  dchrfi  27182  dchreq  27185  dchrresb  27186  dchrinv  27188  dchr1re  27190  sumdchr2  27197  dchr2sum  27200  lgsqrlem2  27274  lgsqrlem3  27275  rpvmasum2  27439  dchrisum0re  27440  mirf1o  28632  lmif1o  28758  eqeefv  28866  axlowdimlem14  28918  vtxdgfisf  29440  2pthon3v  29906  nvinvfval  30602  sspg  30690  ssps  30692  sspmlem  30694  sspn  30698  lnon0  30760  ubthlem1  30832  pjfn  31671  kbpj  31918  kbass2  32079  elpjrn  32152  ofrn2  32597  off2  32598  ofresid  32599  xppreima2  32608  ofpreima2  32623  suppovss  32637  resf1o  32686  prodindf  32819  indpreima  32821  swrdrn3  32910  pwrssmgc  32955  mgcf1o  32958  chnso  32969  gsumfs2d  33021  gsumhashmul  33027  symgcom2  33039  pmtrcnel  33044  pmtrcnel2  33045  pmtrcnelor  33046  cycpmfvlem  33067  cycpmfv3  33070  cycpmcl  33071  cycpmco2rn  33080  cycpmco2  33088  cycpm3cl2  33091  cyc3co2  33095  cyc3evpm  33105  elrgspnlem1  33192  elrgspnlem2  33193  elrgspnlem4  33195  elrgspnsubrunlem1  33197  elrgspnsubrunlem2  33198  islinds5  33314  ellspds  33315  elrspunidl  33375  elrspunsn  33376  rhmimaidl  33379  rhmpreimaprmidl  33398  rprmdvdsprod  33481  1arithidomlem2  33483  evls1fn  33505  ply1dg1rt  33524  ply1mulrtss  33526  ply1degltel  33536  ply1degleel  33537  ply1degltlss  33538  ply1gsumz  33540  ig1pmindeg  33543  r1pquslmic  33552  exsslsb  33568  ply1degltdimlem  33594  ply1degltdim  33595  dimkerim  33599  fedgmullem2  33602  fedgmul  33603  lvecendof1f1o  33605  fldextrspunlsplem  33644  fldextrspunlsp  33645  irngss  33658  irngnzply1  33662  irngnminplynz  33678  2sqr3minply  33746  cos9thpiminply  33754  cmpcref  33816  rhmpreimacnlem  33850  fsumcvg4  33916  pl1cn  33921  qqhval2lem  33947  esumcvg  34052  ofcf  34069  ofcof  34073  measfn  34170  meascnbl  34185  sibfof  34307  sitgaddlemb  34315  subiwrdlen  34353  rrvfn  34412  plymul02  34513  signsplypnf  34517  signsply0  34518  reprsuc  34582  reprdifc  34594  breprexplema  34597  circlemethhgt  34610  hgt750lemb  34623  f1resrcmplf1dlem  35052  pthhashvtx  35100  cvmopnlem  35250  cvmliftmolem1  35253  cvmliftlem10  35266  cvmlift2lem9a  35275  cvmlift2lem6  35280  cvmlift2lem12  35286  cvmliftphtlem  35289  cvmlift3lem9  35299  mrsubrn  35485  elmrsubrn  35492  elmsubrn  35500  msubrn  35501  mclsind  35542  mclsppslem  35555  mclspps  35556  iprodefisumlem  35712  weiunfrlem  36437  matunitlindflem1  37595  poimirlem1  37600  poimirlem2  37601  poimirlem3  37602  poimirlem16  37615  poimirlem17  37616  poimirlem19  37618  poimirlem20  37619  poimirlem22  37621  poimirlem23  37622  poimirlem29  37628  poimirlem30  37629  poimirlem31  37630  poimir  37632  mblfinlem2  37637  itg2addnclem3  37652  itg2addnc  37653  itg2gt0cn  37654  ftc1cnnc  37671  ftc1anclem5  37676  ftc1anclem7  37678  ftc1anc  37680  sdclem2  37721  istotbnd3  37750  sstotbnd2  37753  isbnd3  37763  heibor1lem  37788  rrnmet  37808  grpokerinj  37872  isdrngo2  37937  lfl1  39048  lfladdcl  39049  lflvscl  39055  lkr0f  39072  lkrsc  39075  eqlkr2  39078  eqlkr3  39079  ldualvaddval  39109  ldualvsval  39116  tendoeq1  40743  zndvdchrrhm  41945  hashscontpow  42095  aks6d1c3  42096  aks6d1c2lem4  42100  aks6d1c2  42103  sticksstones1  42119  sticksstones2  42120  sticksstones3  42121  sticksstones12a  42130  sticksstones12  42131  aks6d1c6lem2  42144  aks6d1c6lem3  42145  aks6d1c6isolem1  42147  aks6d1c6isolem3  42149  aks6d1c6lem5  42150  aks6d1c7lem1  42153  unitscyglem1  42168  dvun  42332  frlmvscadiccat  42479  fiabv  42509  frlmsnic  42513  pwsgprod  42517  mplmapghm  42529  evlsvvval  42536  evlsaddval  42541  evlsmulval  42542  evladdval  42548  evlmulval  42549  selvvvval  42558  evlselvlem  42559  evlselv  42560  fsuppssind  42566  mhphf  42570  ismrcd1  42671  ismrcd2  42672  istopclsd  42673  isnacs3  42683  mzpaddmpt  42714  mzpmulmpt  42715  mzpsubst  42721  mzpcong  42945  fnwe2lem2  43024  islmodfg  43042  kercvrlsm  43056  dgrsub2  43108  mpaaeu  43123  rngunsnply  43142  hausgraph  43178  ofoafg  43327  ofoafo  43329  ofoaid1  43331  ofoaid2  43332  naddcnff  43335  naddcnffn  43336  naddcnffo  43337  naddcnfcom  43339  naddcnfid1  43340  naddcnfass  43342  fsovf1od  43989  brcoffn  44003  clsneiel1  44081  wfximgfd  44136  extoimad  44137  mnringmulrcld  44201  mnurndlem1  44254  caofcan  44296  ofmul12  44298  ofdivrec  44299  ofdivcan4  44300  ofdivdiv2  44301  dvconstbi  44307  binomcxplemnotnn0  44329  relpmin  44926  refsum2cnlem1  45015  ssmapsn  45194  preimaiocmnf  45542  fsumsupp0  45560  fsumsermpt  45561  climinf  45588  climinf2lem  45688  limsupmnflem  45702  limsupvaluz2  45720  supcnvlimsup  45722  limsupgtlem  45759  liminfvalxr  45765  liminflelimsupuz  45767  xlimconst2  45817  climxlim2  45828  icccncfext  45869  dvnprodlem1  45928  volicoff  45977  voliooicof  45978  fourierdlem25  46114  etransclem2  46218  etransclem35  46251  fge0iccico  46352  sge0tsms  46362  sge0sup  46373  sge0resrn  46386  sge0le  46389  sge0fodjrnlem  46398  sge0isum  46409  sge0seq  46428  nnfoctbdjlem  46437  meadjiunlem  46447  omeiunle  46499  hoicvr  46530  ovolval4lem1  46631  ovolval5lem3  46636  ovnovollem1  46638  ovnovollem2  46639  iinhoiicclem  46655  iunhoiioolem  46657  preimaicomnf  46693  smfresal  46770  smfsuplem1  46793  smflimsuplem2  46803  fcoreslem3  47050  fcoreslem4  47051  fcores  47052  isubgredg  47851  upgrimpths  47894  ackvalsucsucval  48674  funchomf  49083  imasubc  49137  imassc  49139  imaid  49140  prcofdiag1  49379  prcofdiag  49380  oppfdiag1  49400  oppfdiag  49402  amgmwlem  49788