Theorem ffnd 6663

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

Syntax hints:   → wi 4   Fn wfn 6487  ⟶wf 6488

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 208  df-an 397  df-f 6496

This theorem is referenced by:  fnconstg  6722  f1fn  6731  fofn  6748  f1ofn  6775  feqmptd  6902  fssrescdmd  7075  fprb  7145  cocan1  7242  oprres  7531  off  7645  coof  7651  ofco  7652  caofref  7658  caofid0l  7660  caofid0r  7661  caofid1  7662  caofid2  7663  caofrss  7666  caoftrn  7668  fo2ndf  8067  fnwelem  8078  fnse  8080  suppsnop  8125  suppss  8141  suppssr  8142  suppssrg  8143  suppssof1  8146  suppofssd  8150  suppofss1d  8151  suppofss2d  8152  suppcoss  8154  smocdmdom  8305  elmapfn  8809  ralxpmap  8841  omxpenlem  9013  mapen  9076  f1finf1o  9180  unirnffid  9254  fdmfifsupp  9285  mapfien  9318  intrnfi  9326  marypha2  9349  ordtypelem7  9436  wemapsolem  9462  wemapso  9463  wemapso2lem  9464  unxpwdom2  9500  ixpiunwdom  9502  cantnfle  9590  cantnfp1lem2  9598  cantnfp1lem3  9599  cantnfp1  9600  oemapvali  9603  cantnflem1a  9604  cantnflem1c  9606  cantnflem3  9610  cantnf  9612  cnfcomlem  9618  cnfcom3  9623  updjudhcoinlf  9854  updjudhcoinrg  9855  fseqenlem1  9944  numacn  9969  infpwfien  9982  isf32lem2  10274  isf34lem7  10299  isf34lem6  10300  unirnfdomd  10488  ofsubeq0  12154  ofnegsub  12155  ofsubge0  12156  seqf1olem2  14002  resunimafz0  14405  wrdfn  14488  swrdvalfn  14612  pfxfn  14642  pfxid  14645  cats1un  14681  cshwfn  14761  ccatco  14795  limsupgle  15437  o1of2  15573  o1rlimmul  15579  isercolllem2  15626  isercoll  15628  isercoll2  15629  climsup  15630  fsumss  15685  ruclem11  16205  vdwlem2  16951  vdwlem6  16955  vdwlem9  16958  vdwlem12  16961  0ram  16989  ramub1lem1  16995  pwsle  17454  pwsleval  17455  pwsvscaval  17457  mrcuni  17585  mrcun  17586  invf1o  17734  funcres2c  17868  setcmon  18052  setcepi  18053  uncfcurf  18203  yoniso  18249  isacs4lem  18508  acsmapd  18518  chnso  18588  gsumval2  18652  mgmhmf1o  18666  resmgmhm2b  18679  mgmhmima  18681  mgmhmeql  18682  prdsplusgsgrpcl  18698  prdssgrpd  18699  prdsplusgcl  18734  prdsidlem  18735  prdsmndd  18736  mhmf1o  18762  resmhm2b  18788  mhmimalem  18790  mhmima  18791  mhmeql  18792  prdspjmhm  18795  pwsco1mhm  18798  pwsco2mhm  18799  gsumwmhm  18811  frmdss2  18829  grpinvf1o  18983  prdsinvlem  19023  cycsubgcl  19179  ghmrn  19202  ghmpreima  19211  ghmeql  19212  ghmnsgima  19213  ghmnsgpreima  19214  ghmeqker  19216  ghmf1o  19221  ghmqusnsglem1  19253  ghmqusnsg  19255  ghmquskerlem1  19256  ghmquskerco  19257  ghmquskerlem3  19259  ghmqusker  19260  gass  19274  cntzmhm  19314  symgextres  19398  gsmsymgrfixlem1  19400  fvcosymgeq  19402  f1omvdconj  19419  pmtrfinv  19434  symgtrinv  19445  pmtr3ncomlem1  19446  sygbasnfpfi  19485  efginvrel2  19700  efgredleme  19716  ghmplusg  19819  prdscmnd  19834  gsumval3a  19876  gsumval3eu  19877  gsumzaddlem  19894  gsumzsplit  19900  gsumpt  19935  prdsgsum  19954  dprdfcntz  19990  dprdfadd  19995  dprdfeq0  19997  dprdf11  19998  dprdlub  20001  dprdspan  20002  dprd2dlem1  20016  dmdprdpr  20024  dprdpr  20025  dpjlem  20026  ablfac1eu  20048  gsumle  20118  prdsmulrngcl  20154  prdsrngd  20155  prdsringd  20298  prdscrngd  20299  prds1  20300  pwspjmhmmgpd  20305  pwsgprod  20307  rnghmf1o  20430  rhmf1o  20469  rhmimasubrnglem  20544  rnrhmsubrg  20584  rrgsupp  20680  imadrhmcl  20776  isabvd  20791  lmodfopnelem1  20895  lcomfsupp  20899  prdsvscacl  20965  prdslmodd  20966  lmhmco  21040  lmhmplusg  21041  lmhmvsca  21042  lmhmf1o  21043  lmhmeql  21052  lspextmo  21053  rhmpreimaidl  21277  pjfo  21697  dsmmbas2  21719  dsmm0cl  21722  dsmmacl  21723  dsmmsubg  21725  dsmmlss  21726  frlmvplusgvalc  21749  frlmvscaval  21750  frlmplusgvalb  21751  frlmvscavalb  21752  frlmsslss2  21757  frlmphllem  21762  frlmphl  21763  frlmssuvc2  21777  frlmsslsp  21778  frlmup1  21780  frlmup2  21781  frlmup3  21782  frlmup4  21783  islindf4  21820  psrbagfsupp  21901  psrbaglesupp  21904  psrbaglecl  21905  psrbagaddcl  21906  psrbagcon  21907  psrbaglefi  21908  psrbagleadd1  21910  psrbagconf1o  21911  gsumbagdiaglem  21913  psrass1lem  21915  psrvscaval  21932  psrlidm  21943  psrridm  21944  psrass1  21945  psrdi  21946  psrdir  21947  psrascl  21960  mvrf2  21974  mplsubglem  21980  mplvscaval  21997  subrgmvrf  22017  mplbas2  22025  mplind  22053  psrbagev1  22060  psrbagev2  22061  evlslem3  22063  evlslem1  22065  evlsvvval  22076  evlsvar  22078  evladdval  22086  evlmulval  22087  mpfind  22098  mplmapghm  22105  evlsaddval  22112  evlsmulval  22113  selvvvval  22125  ismhp3  22137  mhpmulcl  22144  psdmplcl  22157  psdadd  22158  psdvsca  22159  psdmul  22161  psdmvr  22164  psrplusgpropd  22227  coe1add  22257  coe1addfv  22258  evl1addd  22334  evl1subd  22335  evl1muld  22336  pf1mpf  22345  pf1ind  22348  evls1fpws  22362  ressply1evl  22363  rhmply1vsca  22378  mamudir  22394  mamulid  22431  mamurid  22432  mdetrlin  22592  mdetrsca  22593  mdetralt  22598  mdetunilem7  22608  mdetunilem9  22610  madurid  22634  cnrest2  23276  lmss  23288  lmcnp  23294  cnt0  23336  cnt1  23340  cnhaus  23344  rncmp  23386  conncn  23416  2ndcomap  23448  1stccnp  23452  comppfsc  23522  1stckgenlem  23543  ptbasfi  23571  ptopn  23573  ptclsg  23605  ptcnp  23612  upxp  23613  txtube  23630  txcmplem1  23631  hauseqlcld  23636  xkohaus  23643  xkoptsub  23644  cnmpt11  23653  cnmpt21  23661  cnmpt22f  23665  cnmptcom  23668  qtopss  23705  qtopeu  23706  qtopomap  23708  qtopcmap  23709  kqffn  23715  hmeof1o2  23753  xkocnv  23804  rnelfm  23943  ptcmplem1  24042  cnextfres1  24058  ghmcnp  24105  tgphaus  24107  prdstmdd  24114  prdstgpd  24115  fmucnd  24281  psmetxrge0  24303  isxmet2d  24317  prdsmet  24360  blelrnps  24406  blelrn  24407  xmetresbl  24427  comet  24503  stdbdxmet  24505  met2ndci  24512  prdsxmslem2  24519  isngp3  24588  nmotri  24729  metdsre  24844  bndth  24950  evth  24951  fmcfil  25264  bcthlem4  25319  rrxcph  25384  rrxds  25385  rrxmet  25400  evthicc2  25452  ovolfsf  25463  ovolmge0  25469  ovollb2lem  25480  ovolunlem1a  25488  ovoliunlem1  25494  ovoliun  25497  ovoliun2  25498  ovolscalem1  25505  ovolicc1  25508  ovolicc2lem4  25512  ovolicc2  25514  voliunlem1  25542  voliunlem3  25544  volsup  25548  ioombl1lem2  25551  ioombl1lem4  25553  uniiccdif  25570  uniioombllem2  25575  uniioombllem3  25577  uniioombllem6  25580  volsup2  25597  vitalilem4  25603  mbfeqalem1  25633  mbfmulc2lem  25639  mbfmax  25641  mbfaddlem  25652  mbfadd  25653  mbfsub  25654  mbfsup  25656  mbfinf  25657  itg1ge0  25678  itg1addlem1  25684  i1faddlem  25685  i1fmullem  25686  i1fadd  25687  i1fmul  25688  itg1addlem4  25691  i1fmulclem  25694  i1fmulc  25695  itg1mulc  25696  i1fres  25697  itg10a  25702  itg1ge0a  25703  itg1lea  25704  mbfi1fseqlem3  25709  mbfi1fseqlem4  25710  mbfi1flimlem  25714  mbfmullem2  25716  mbfmul  25718  itg20  25729  itg2lea  25736  itg2splitlem  25740  itg2split  25741  itg2monolem1  25742  itg2monolem2  25743  itg2monolem3  25744  itg2mono  25745  itg2i1fseqle  25746  itg2i1fseq  25747  itg2addlem  25750  itg2gt0  25752  itg2cnlem1  25753  itg2cnlem2  25754  itg2cn  25755  itgitg1  25801  bddmulibl  25831  bddibl  25832  dvidlem  25907  dvaddbr  25930  dvmulbr  25931  dvaddf  25934  dvcmulf  25937  dvrec  25947  dvcnvlem  25968  rolle  25982  dveq0  25992  dv11cn  25993  dvivthlem2  26001  dvivth  26002  dvne0  26003  lhop1lem  26005  lhop1  26006  lhop2  26007  lhop  26008  ftc1cn  26035  tdeglem1  26048  tdeglem3  26049  tdeglem4  26050  mdegleb  26054  mdegldg  26056  mdegaddle  26064  ply1remlem  26155  ply1rem  26156  fta1glem1  26158  fta1glem2  26159  fta1blem  26161  idomrootle  26163  plyeq0lem  26200  plyeq0  26201  plyaddlem1  26203  coeeulem  26214  coeaddlem  26239  coemulc  26245  dgradd2  26258  dgrcolem2  26264  ofmulrt  26273  plyrem  26296  vieta1lem1  26301  vieta1  26303  plyexmo  26304  elqaalem3  26312  aannenlem1  26319  aalioulem2  26324  ulmuni  26382  ulmdvlem1  26390  ulmdv  26393  mbfulm  26396  iblulm  26397  itgulm  26398  rlimcnp2  26955  jensen  26977  amgm  26979  basellem3  27071  basellem7  27075  basellem9  27077  dchrelbas2  27225  dchrmulcl  27237  dchrfi  27243  dchreq  27246  dchrresb  27247  dchrinv  27249  dchr1re  27251  sumdchr2  27258  dchr2sum  27261  lgsqrlem2  27335  lgsqrlem3  27336  rpvmasum2  27500  dchrisum0re  27501  mirf1o  28762  lmif1o  28888  eqeefv  28997  axlowdimlem14  29049  vtxdgfisf  29570  2pthon3v  30036  nvinvfval  30736  sspg  30824  ssps  30826  sspmlem  30828  sspn  30832  lnon0  30894  ubthlem1  30966  pjfn  31805  kbpj  32052  kbass2  32213  elpjrn  32286  ofrn2  32739  off2  32740  ofresid  32741  xppreima2  32750  ofpreima2  32765  suppovss  32780  resf1o  32829  prodindf  32948  indpreima  32951  swrdrn3  33041  pwrssmgc  33086  mgcf1o  33089  gsumfs2d  33149  gsumhashmul  33155  symgcom2  33172  pmtrcnel  33177  pmtrcnel2  33178  pmtrcnelor  33179  cycpmfvlem  33200  cycpmfv3  33203  cycpmcl  33204  cycpmco2rn  33213  cycpmco2  33221  cycpm3cl2  33224  cyc3co2  33228  cyc3evpm  33238  elrgspnlem1  33330  elrgspnlem2  33331  elrgspnlem4  33333  elrgspnsubrunlem1  33335  elrgspnsubrunlem2  33336  gsumind  33435  islinds5  33457  ellspds  33458  elrspunidl  33518  elrspunsn  33519  rhmimaidl  33522  rhmpreimaprmidl  33541  rprmdvdsprod  33624  1arithidomlem2  33626  evls1fn  33650  ply1dg1rt  33670  ply1mulrtss  33672  ply1degltel  33684  ply1degleel  33685  ply1degltlss  33686  ply1gsumz  33689  ig1pmindeg  33692  r1pquslmic  33701  0mplrim  33705  mplasclco  33707  selvply1rhmlema  33709  selvply1rhmlemb  33710  selvply1rhmlem1  33711  selvply1rhmlem4  33714  selvply1rhm0  33717  extvfvcl  33727  mplmulmvr  33730  evlextv  33733  mplvrpmmhm  33737  mplvrpmrhm  33738  psrmonprod  33743  esplyfval0  33755  esplyfval2  33756  esplyfv1  33760  esplyfv  33761  esplyfval3  33763  esplyfvaln  33765  esplyind  33766  vieta  33771  exsslsb  33788  ply1degltdimlem  33813  ply1degltdim  33814  dimkerim  33818  fedgmullem2  33821  fedgmul  33822  lvecendof1f1o  33824  fldextrspunlsplem  33864  fldextrspunlsp  33865  irngss  33878  irngnzply1  33882  extdgfialglem2  33884  irngnminplynz  33903  2sqr3minply  33971  cos9thpiminply  33979  cmpcref  34041  rhmpreimacnlem  34075  fsumcvg4  34141  pl1cn  34146  qqhval2lem  34172  esumcvg  34277  ofcf  34294  ofcof  34298  measfn  34395  meascnbl  34410  sibfof  34531  sitgaddlemb  34539  subiwrdlen  34577  rrvfn  34636  plymul02  34737  signsplypnf  34741  signsply0  34742  reprsuc  34806  reprdifc  34818  breprexplema  34821  circlemethhgt  34834  hgt750lemb  34847  f1resrcmplf1dlem  35274  pthhashvtx  35363  cvmopnlem  35513  cvmliftmolem1  35516  cvmliftlem10  35529  cvmlift2lem9a  35538  cvmlift2lem6  35543  cvmlift2lem12  35549  cvmliftphtlem  35552  cvmlift3lem9  35562  mrsubrn  35748  elmrsubrn  35755  elmsubrn  35763  msubrn  35764  mclsind  35805  mclsppslem  35818  mclspps  35819  iprodefisumlem  35975  weiunfrlem  36699  mh-inf3f1  36776  matunitlindflem1  37990  poimirlem1  37995  poimirlem2  37996  poimirlem3  37997  poimirlem16  38010  poimirlem17  38011  poimirlem19  38013  poimirlem20  38014  poimirlem22  38016  poimirlem23  38017  poimirlem29  38023  poimirlem30  38024  poimirlem31  38025  poimir  38027  mblfinlem2  38032  itg2addnclem3  38047  itg2addnc  38048  itg2gt0cn  38049  ftc1cnnc  38066  ftc1anclem5  38071  ftc1anclem7  38073  ftc1anc  38075  sdclem2  38116  istotbnd3  38145  sstotbnd2  38148  isbnd3  38158  heibor1lem  38183  rrnmet  38203  grpokerinj  38267  isdrngo2  38332  lfl1  39569  lfladdcl  39570  lflvscl  39576  lkr0f  39593  lkrsc  39596  eqlkr2  39599  eqlkr3  39600  ldualvaddval  39630  ldualvsval  39637  tendoeq1  41263  zndvdchrrhm  42465  hashscontpow  42614  aks6d1c3  42615  aks6d1c2lem4  42619  aks6d1c2  42622  sticksstones1  42638  sticksstones2  42639  sticksstones3  42640  sticksstones12a  42649  sticksstones12  42650  aks6d1c6lem2  42663  aks6d1c6lem3  42664  aks6d1c6isolem1  42666  aks6d1c6isolem3  42668  aks6d1c6lem5  42669  aks6d1c7lem1  42672  unitscyglem1  42687  dvun  42843  frlmvscadiccat  43003  fiabv  43029  frlmsnic  43033  evlselvlem  43045  evlselv  43046  fsuppssind  43050  mhphf  43054  ismrcd1  43154  ismrcd2  43155  istopclsd  43156  isnacs3  43166  mzpaddmpt  43197  mzpmulmpt  43198  mzpsubst  43204  mzpcong  43424  fnwe2lem2  43503  islmodfg  43521  kercvrlsm  43535  dgrsub2  43587  mpaaeu  43602  rngunsnply  43621  hausgraph  43657  ofoafg  43806  ofoafo  43808  ofoaid1  43810  ofoaid2  43811  naddcnff  43814  naddcnffn  43815  naddcnffo  43816  naddcnfcom  43818  naddcnfid1  43819  naddcnfass  43821  fsovf1od  44467  brcoffn  44481  clsneiel1  44559  wfximgfd  44614  extoimad  44615  mnringmulrcld  44679  mnurndlem1  44732  caofcan  44774  ofmul12  44776  ofdivrec  44777  ofdivcan4  44778  ofdivdiv2  44779  dvconstbi  44785  binomcxplemnotnn0  44807  relpmin  45403  refsum2cnlem1  45492  ssmapsn  45668  preimaiocmnf  46012  fsumsupp0  46030  fsumsermpt  46031  climinf  46058  climinf2lem  46156  limsupmnflem  46170  limsupvaluz2  46188  supcnvlimsup  46190  limsupgtlem  46227  liminfvalxr  46233  liminflelimsupuz  46235  xlimconst2  46285  climxlim2  46296  icccncfext  46337  dvnprodlem1  46396  volicoff  46445  voliooicof  46446  fourierdlem25  46582  etransclem2  46686  etransclem35  46719  fge0iccico  46820  sge0tsms  46830  sge0sup  46841  sge0resrn  46854  sge0le  46857  sge0fodjrnlem  46866  sge0isum  46877  sge0seq  46896  nnfoctbdjlem  46905  meadjiunlem  46915  omeiunle  46967  hoicvr  46998  ovolval4lem1  47099  ovolval5lem3  47104  ovnovollem1  47106  ovnovollem2  47107  iinhoiicclem  47123  iunhoiioolem  47125  preimaicomnf  47161  smfresal  47238  smfsuplem1  47261  smflimsuplem2  47271  fcoreslem3  47535  fcoreslem4  47536  fcores  47537  isubgredg  48364  upgrimpths  48407  ackvalsucsucval  49186  funchomf  49594  imasubc  49648  imassc  49650  imaid  49651  prcofdiag1  49890  prcofdiag  49891  oppfdiag1  49911  oppfdiag  49913  amgmwlem  50299