Theorem ffnd 6692

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

Syntax hints:   → wi 4   Fn wfn 6509  ⟶wf 6510

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 6518

This theorem is referenced by:  fnconstg  6751  f1fn  6760  fofn  6777  f1ofn  6804  feqmptd  6932  fssrescdmd  7101  fprb  7171  cocan1  7269  oprres  7560  off  7674  coof  7680  ofco  7681  caofref  7687  caofid0l  7689  caofid0r  7690  caofid1  7691  caofid2  7692  caofrss  7695  caoftrn  7697  fo2ndf  8103  fnwelem  8113  fnse  8115  suppsnop  8160  suppss  8176  suppssr  8177  suppssrg  8178  suppssof1  8181  suppofssd  8185  suppofss1d  8186  suppofss2d  8187  suppcoss  8189  smocdmdom  8340  elmapfn  8841  ralxpmap  8872  omxpenlem  9047  mapen  9111  f1finf1o  9223  f1finf1oOLD  9224  unirnffid  9305  fdmfifsupp  9333  mapfien  9366  intrnfi  9374  marypha2  9397  ordtypelem7  9484  wemapsolem  9510  wemapso  9511  wemapso2lem  9512  unxpwdom2  9548  ixpiunwdom  9550  cantnfle  9631  cantnfp1lem2  9639  cantnfp1lem3  9640  cantnfp1  9641  oemapvali  9644  cantnflem1a  9645  cantnflem1c  9647  cantnflem3  9651  cantnf  9653  cnfcomlem  9659  cnfcom3  9664  updjudhcoinlf  9892  updjudhcoinrg  9893  fseqenlem1  9984  numacn  10009  infpwfien  10022  isf32lem2  10314  isf34lem7  10339  isf34lem6  10340  unirnfdomd  10527  ofsubeq0  12190  ofnegsub  12191  ofsubge0  12192  seqf1olem2  14014  resunimafz0  14417  wrdfn  14500  swrdvalfn  14623  pfxfn  14653  pfxid  14656  cats1un  14693  cshwfn  14773  ccatco  14808  limsupgle  15450  o1of2  15586  o1rlimmul  15592  isercolllem2  15639  isercoll  15641  isercoll2  15642  climsup  15643  fsumss  15698  ruclem11  16215  vdwlem2  16960  vdwlem6  16964  vdwlem9  16967  vdwlem12  16970  0ram  16998  ramub1lem1  17004  pwsle  17462  pwsleval  17463  pwsvscaval  17465  mrcuni  17589  mrcun  17590  invf1o  17738  funcres2c  17872  setcmon  18056  setcepi  18057  uncfcurf  18207  yoniso  18253  isacs4lem  18510  acsmapd  18520  gsumval2  18620  mgmhmf1o  18634  resmgmhm2b  18647  mgmhmima  18649  mgmhmeql  18650  prdsplusgsgrpcl  18666  prdssgrpd  18667  prdsplusgcl  18702  prdsidlem  18703  prdsmndd  18704  mhmf1o  18730  resmhm2b  18756  mhmimalem  18758  mhmima  18759  mhmeql  18760  prdspjmhm  18763  pwsco1mhm  18766  pwsco2mhm  18767  gsumwmhm  18779  frmdss2  18797  grpinvf1o  18948  prdsinvlem  18988  cycsubgcl  19145  ghmrn  19168  ghmpreima  19177  ghmeql  19178  ghmnsgima  19179  ghmnsgpreima  19180  ghmeqker  19182  ghmf1o  19187  ghmqusnsglem1  19219  ghmqusnsg  19221  ghmquskerlem1  19222  ghmquskerco  19223  ghmquskerlem3  19225  ghmqusker  19226  gass  19240  cntzmhm  19280  symgextres  19362  gsmsymgrfixlem1  19364  fvcosymgeq  19366  f1omvdconj  19383  pmtrfinv  19398  symgtrinv  19409  pmtr3ncomlem1  19410  sygbasnfpfi  19449  efginvrel2  19664  efgredleme  19680  ghmplusg  19783  prdscmnd  19798  gsumval3a  19840  gsumval3eu  19841  gsumzaddlem  19858  gsumzsplit  19864  gsumpt  19899  prdsgsum  19918  dprdfcntz  19954  dprdfadd  19959  dprdfeq0  19961  dprdf11  19962  dprdlub  19965  dprdspan  19966  dprd2dlem1  19980  dmdprdpr  19988  dprdpr  19989  dpjlem  19990  ablfac1eu  20012  prdsmulrngcl  20091  prdsrngd  20092  prdsringd  20237  prdscrngd  20238  prds1  20239  pwspjmhmmgpd  20244  rnghmf1o  20368  rhmf1o  20407  rhmimasubrnglem  20481  rnrhmsubrg  20521  rrgsupp  20617  imadrhmcl  20713  isabvd  20728  lmodfopnelem1  20811  lcomfsupp  20815  prdsvscacl  20881  prdslmodd  20882  lmhmco  20957  lmhmplusg  20958  lmhmvsca  20959  lmhmf1o  20960  lmhmeql  20969  lspextmo  20970  rhmpreimaidl  21194  pjfo  21631  dsmmbas2  21653  dsmm0cl  21656  dsmmacl  21657  dsmmsubg  21659  dsmmlss  21660  frlmvplusgvalc  21683  frlmvscaval  21684  frlmplusgvalb  21685  frlmvscavalb  21686  frlmsslss2  21691  frlmphllem  21696  frlmphl  21697  frlmssuvc2  21711  frlmsslsp  21712  frlmup1  21714  frlmup2  21715  frlmup3  21716  frlmup4  21717  islindf4  21754  psrbagfsupp  21835  psrbaglesupp  21838  psrbaglecl  21839  psrbagaddcl  21840  psrbagcon  21841  psrbaglefi  21842  psrbagleadd1  21844  psrbagconf1o  21845  gsumbagdiaglem  21846  psrass1lem  21848  psrvscaval  21866  psrlidm  21878  psrridm  21879  psrass1  21880  psrdi  21881  psrdir  21882  psrascl  21895  mvrf2  21909  mplsubglem  21915  mplvscaval  21932  subrgmvrf  21948  mplbas2  21956  mplind  21984  psrbagev1  21991  psrbagev2  21992  evlslem3  21994  evlslem1  21996  evlsvar  22004  mpfind  22021  ismhp3  22036  mhpmulcl  22043  psdmplcl  22056  psdadd  22057  psdvsca  22058  psdmul  22060  psdmvr  22063  psrplusgpropd  22127  coe1add  22157  coe1addfv  22158  evl1addd  22235  evl1subd  22236  evl1muld  22237  pf1mpf  22246  pf1ind  22249  evls1fpws  22263  ressply1evl  22264  rhmply1vsca  22282  mamudir  22298  mamulid  22335  mamurid  22336  mdetrlin  22496  mdetrsca  22497  mdetralt  22502  mdetunilem7  22512  mdetunilem9  22514  madurid  22538  cnrest2  23180  lmss  23192  lmcnp  23198  cnt0  23240  cnt1  23244  cnhaus  23248  rncmp  23290  conncn  23320  2ndcomap  23352  1stccnp  23356  comppfsc  23426  1stckgenlem  23447  ptbasfi  23475  ptopn  23477  ptclsg  23509  ptcnp  23516  upxp  23517  txtube  23534  txcmplem1  23535  hauseqlcld  23540  xkohaus  23547  xkoptsub  23548  cnmpt11  23557  cnmpt21  23565  cnmpt22f  23569  cnmptcom  23572  qtopss  23609  qtopeu  23610  qtopomap  23612  qtopcmap  23613  kqffn  23619  hmeof1o2  23657  xkocnv  23708  rnelfm  23847  ptcmplem1  23946  cnextfres1  23962  ghmcnp  24009  tgphaus  24011  prdstmdd  24018  prdstgpd  24019  fmucnd  24186  psmetxrge0  24208  isxmet2d  24222  prdsmet  24265  blelrnps  24311  blelrn  24312  xmetresbl  24332  comet  24408  stdbdxmet  24410  met2ndci  24417  prdsxmslem2  24424  isngp3  24493  nmotri  24634  metdsre  24749  bndth  24864  evth  24865  fmcfil  25179  bcthlem4  25234  rrxcph  25299  rrxds  25300  rrxmet  25315  evthicc2  25368  ovolfsf  25379  ovolmge0  25385  ovollb2lem  25396  ovolunlem1a  25404  ovoliunlem1  25410  ovoliun  25413  ovoliun2  25414  ovolscalem1  25421  ovolicc1  25424  ovolicc2lem4  25428  ovolicc2  25430  voliunlem1  25458  voliunlem3  25460  volsup  25464  ioombl1lem2  25467  ioombl1lem4  25469  uniiccdif  25486  uniioombllem2  25491  uniioombllem3  25493  uniioombllem6  25496  volsup2  25513  vitalilem4  25519  mbfeqalem1  25549  mbfmulc2lem  25555  mbfmax  25557  mbfaddlem  25568  mbfadd  25569  mbfsub  25570  mbfsup  25572  mbfinf  25573  itg1ge0  25594  itg1addlem1  25600  i1faddlem  25601  i1fmullem  25602  i1fadd  25603  i1fmul  25604  itg1addlem4  25607  i1fmulclem  25610  i1fmulc  25611  itg1mulc  25612  i1fres  25613  itg10a  25618  itg1ge0a  25619  itg1lea  25620  mbfi1fseqlem3  25625  mbfi1fseqlem4  25626  mbfi1flimlem  25630  mbfmullem2  25632  mbfmul  25634  itg20  25645  itg2lea  25652  itg2splitlem  25656  itg2split  25657  itg2monolem1  25658  itg2monolem2  25659  itg2monolem3  25660  itg2mono  25661  itg2i1fseqle  25662  itg2i1fseq  25663  itg2addlem  25666  itg2gt0  25668  itg2cnlem1  25669  itg2cnlem2  25670  itg2cn  25671  itgitg1  25717  bddmulibl  25747  bddibl  25748  dvidlem  25823  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  dvaddf  25852  dvcmulf  25855  dvrec  25866  dvcnvlem  25887  rolle  25901  dveq0  25912  dv11cn  25913  dvivthlem2  25921  dvivth  25922  dvne0  25923  lhop1lem  25925  lhop1  25926  lhop2  25927  lhop  25928  ftc1cn  25957  tdeglem1  25970  tdeglem3  25971  tdeglem4  25972  mdegleb  25976  mdegldg  25978  mdegaddle  25986  ply1remlem  26077  ply1rem  26078  fta1glem1  26080  fta1glem2  26081  fta1blem  26083  idomrootle  26085  plyeq0lem  26122  plyeq0  26123  plyaddlem1  26125  coeeulem  26136  coeaddlem  26161  coemulc  26167  dgradd2  26181  dgrcolem2  26187  ofmulrt  26196  plyrem  26220  vieta1lem1  26225  vieta1  26227  plyexmo  26228  elqaalem3  26236  aannenlem1  26243  aalioulem2  26248  ulmuni  26308  ulmdvlem1  26316  ulmdv  26319  mbfulm  26322  iblulm  26323  itgulm  26324  rlimcnp2  26883  jensen  26906  amgm  26908  basellem3  27000  basellem7  27004  basellem9  27006  dchrelbas2  27155  dchrmulcl  27167  dchrfi  27173  dchreq  27176  dchrresb  27177  dchrinv  27179  dchr1re  27181  sumdchr2  27188  dchr2sum  27191  lgsqrlem2  27265  lgsqrlem3  27266  rpvmasum2  27430  dchrisum0re  27431  mirf1o  28603  lmif1o  28729  eqeefv  28837  axlowdimlem14  28889  vtxdgfisf  29411  2pthon3v  29880  nvinvfval  30576  sspg  30664  ssps  30666  sspmlem  30668  sspn  30672  lnon0  30734  ubthlem1  30806  pjfn  31645  kbpj  31892  kbass2  32053  elpjrn  32126  ofrn2  32571  off2  32572  ofresid  32573  xppreima2  32582  ofpreima2  32597  suppovss  32611  resf1o  32660  prodindf  32793  indpreima  32795  swrdrn3  32884  pwrssmgc  32933  mgcf1o  32936  chnso  32947  gsumfs2d  33002  gsumhashmul  33008  gsumle  33045  symgcom2  33048  pmtrcnel  33053  pmtrcnel2  33054  pmtrcnelor  33055  cycpmfvlem  33076  cycpmfv3  33079  cycpmcl  33080  cycpmco2rn  33089  cycpmco2  33097  cycpm3cl2  33100  cyc3co2  33104  cyc3evpm  33114  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnlem4  33203  elrgspnsubrunlem1  33205  elrgspnsubrunlem2  33206  islinds5  33345  ellspds  33346  elrspunidl  33406  elrspunsn  33407  rhmimaidl  33410  rhmpreimaprmidl  33429  rprmdvdsprod  33512  1arithidomlem2  33514  evls1fn  33536  ply1dg1rt  33555  ply1mulrtss  33557  ply1degltel  33567  ply1degleel  33568  ply1degltlss  33569  ply1gsumz  33571  ig1pmindeg  33574  r1pquslmic  33583  exsslsb  33599  ply1degltdimlem  33625  ply1degltdim  33626  dimkerim  33630  fedgmullem2  33633  fedgmul  33634  lvecendof1f1o  33636  fldextrspunlsplem  33675  fldextrspunlsp  33676  irngss  33689  irngnzply1  33693  irngnminplynz  33709  2sqr3minply  33777  cos9thpiminply  33785  cmpcref  33847  rhmpreimacnlem  33881  fsumcvg4  33947  pl1cn  33952  qqhval2lem  33978  esumcvg  34083  ofcf  34100  ofcof  34104  measfn  34201  meascnbl  34216  sibfof  34338  sitgaddlemb  34346  subiwrdlen  34384  rrvfn  34443  plymul02  34544  signsplypnf  34548  signsply0  34549  reprsuc  34613  reprdifc  34625  breprexplema  34628  circlemethhgt  34641  hgt750lemb  34654  f1resrcmplf1dlem  35083  pthhashvtx  35122  cvmopnlem  35272  cvmliftmolem1  35275  cvmliftlem10  35288  cvmlift2lem9a  35297  cvmlift2lem6  35302  cvmlift2lem12  35308  cvmliftphtlem  35311  cvmlift3lem9  35321  mrsubrn  35507  elmrsubrn  35514  elmsubrn  35522  msubrn  35523  mclsind  35564  mclsppslem  35577  mclspps  35578  iprodefisumlem  35734  weiunfrlem  36459  matunitlindflem1  37617  poimirlem1  37622  poimirlem2  37623  poimirlem3  37624  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem22  37643  poimirlem23  37644  poimirlem29  37650  poimirlem30  37651  poimirlem31  37652  poimir  37654  mblfinlem2  37659  itg2addnclem3  37674  itg2addnc  37675  itg2gt0cn  37676  ftc1cnnc  37693  ftc1anclem5  37698  ftc1anclem7  37700  ftc1anc  37702  sdclem2  37743  istotbnd3  37772  sstotbnd2  37775  isbnd3  37785  heibor1lem  37810  rrnmet  37830  grpokerinj  37894  isdrngo2  37959  lfl1  39070  lfladdcl  39071  lflvscl  39077  lkr0f  39094  lkrsc  39097  eqlkr2  39100  eqlkr3  39101  ldualvaddval  39131  ldualvsval  39138  tendoeq1  40765  zndvdchrrhm  41967  hashscontpow  42117  aks6d1c3  42118  aks6d1c2lem4  42122  aks6d1c2  42125  sticksstones1  42141  sticksstones2  42142  sticksstones3  42143  sticksstones12a  42152  sticksstones12  42153  aks6d1c6lem2  42166  aks6d1c6lem3  42167  aks6d1c6isolem1  42169  aks6d1c6isolem3  42171  aks6d1c6lem5  42172  aks6d1c7lem1  42175  unitscyglem1  42190  dvun  42354  frlmvscadiccat  42501  fiabv  42531  frlmsnic  42535  pwsgprod  42539  mplmapghm  42551  evlsvvval  42558  evlsaddval  42563  evlsmulval  42564  evladdval  42570  evlmulval  42571  selvvvval  42580  evlselvlem  42581  evlselv  42582  fsuppssind  42588  mhphf  42592  ismrcd1  42693  ismrcd2  42694  istopclsd  42695  isnacs3  42705  mzpaddmpt  42736  mzpmulmpt  42737  mzpsubst  42743  mzpcong  42968  fnwe2lem2  43047  islmodfg  43065  kercvrlsm  43079  dgrsub2  43131  mpaaeu  43146  rngunsnply  43165  hausgraph  43201  ofoafg  43350  ofoafo  43352  ofoaid1  43354  ofoaid2  43355  naddcnff  43358  naddcnffn  43359  naddcnffo  43360  naddcnfcom  43362  naddcnfid1  43363  naddcnfass  43365  fsovf1od  44012  brcoffn  44026  clsneiel1  44104  wfximgfd  44159  extoimad  44160  mnringmulrcld  44224  mnurndlem1  44277  caofcan  44319  ofmul12  44321  ofdivrec  44322  ofdivcan4  44323  ofdivdiv2  44324  dvconstbi  44330  binomcxplemnotnn0  44352  relpmin  44949  refsum2cnlem1  45038  ssmapsn  45217  preimaiocmnf  45565  fsumsupp0  45583  fsumsermpt  45584  climinf  45611  climinf2lem  45711  limsupmnflem  45725  limsupvaluz2  45743  supcnvlimsup  45745  limsupgtlem  45782  liminfvalxr  45788  liminflelimsupuz  45790  xlimconst2  45840  climxlim2  45851  icccncfext  45892  dvnprodlem1  45951  volicoff  46000  voliooicof  46001  fourierdlem25  46137  etransclem2  46241  etransclem35  46274  fge0iccico  46375  sge0tsms  46385  sge0sup  46396  sge0resrn  46409  sge0le  46412  sge0fodjrnlem  46421  sge0isum  46432  sge0seq  46451  nnfoctbdjlem  46460  meadjiunlem  46470  omeiunle  46522  hoicvr  46553  ovolval4lem1  46654  ovolval5lem3  46659  ovnovollem1  46661  ovnovollem2  46662  iinhoiicclem  46678  iunhoiioolem  46680  preimaicomnf  46716  smfresal  46793  smfsuplem1  46816  smflimsuplem2  46826  fcoreslem3  47070  fcoreslem4  47071  fcores  47072  isubgredg  47870  upgrimpths  47913  ackvalsucsucval  48681  funchomf  49090  imasubc  49144  imassc  49146  imaid  49147  prcofdiag1  49386  prcofdiag  49387  oppfdiag1  49407  oppfdiag  49409  amgmwlem  49795