Theorem ffnd 6593

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

Syntax hints:   → wi 4   Fn wfn 6421  ⟶wf 6422

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 206  df-an 397  df-f 6430

This theorem is referenced by:  fnconstg  6654  f1fn  6663  fofn  6682  f1ofn  6709  feqmptd  6829  fprb  7061  rnmptcOLD  7075  cocan1  7155  oprres  7430  off  7541  ofco  7546  caofref  7552  caofid0l  7554  caofid0r  7555  caofid1  7556  caofid2  7557  caofrss  7559  caoftrn  7561  fo2ndf  7949  fnwelem  7959  fnse  7961  suppsnop  7981  suppss  7997  suppssOLD  7998  suppssr  7999  suppssrg  8000  suppssof1  8002  suppofssd  8006  suppofss1d  8007  suppofss2d  8008  suppcoss  8010  smorndom  8186  elmapfn  8640  ralxpmap  8671  omxpenlem  8847  mapen  8915  f1finf1o  9033  unirnffid  9098  fdmfifsupp  9125  mapfien  9154  intrnfi  9162  marypha2  9185  ordtypelem7  9270  wemapsolem  9296  wemapso  9297  wemapso2lem  9298  unxpwdom2  9334  ixpiunwdom  9336  cantnfle  9416  cantnfp1lem2  9424  cantnfp1lem3  9425  cantnfp1  9426  oemapvali  9429  cantnflem1a  9430  cantnflem1c  9432  cantnflem3  9436  cantnf  9438  cnfcomlem  9444  cnfcom3  9449  updjudhcoinlf  9700  updjudhcoinrg  9701  fseqenlem1  9790  numacn  9815  infpwfien  9828  isf32lem2  10120  isf34lem7  10145  isf34lem6  10146  unirnfdomd  10333  ofsubeq0  11980  ofnegsub  11981  ofsubge0  11982  seqf1olem2  13773  resunimafz0  14167  wrdfn  14241  swrdvalfn  14374  pfxfn  14404  pfxid  14407  cats1un  14444  cshwfn  14524  ccatco  14558  limsupgle  15196  o1of2  15332  o1rlimmul  15338  isercolllem2  15387  isercoll  15389  isercoll2  15390  climsup  15391  fsumss  15447  ruclem11  15959  vdwlem2  16693  vdwlem6  16697  vdwlem9  16700  vdwlem12  16703  0ram  16731  ramub1lem1  16737  pwsle  17213  pwsleval  17214  pwsvscaval  17216  mrcuni  17340  mrcun  17341  invf1o  17491  funcres2c  17627  setcmon  17812  setcepi  17813  uncfcurf  17967  yoniso  18013  isacs4lem  18272  acsmapd  18282  gsumval2  18380  prdsplusgcl  18426  prdsidlem  18427  prdsmndd  18428  mhmf1o  18450  resmhm2b  18471  mhmima  18473  mhmeql  18474  prdspjmhm  18477  pwsco1mhm  18480  pwsco2mhm  18481  gsumwmhm  18494  frmdss2  18512  grpinvf1o  18655  prdsinvlem  18694  cycsubgcl  18835  ghmrn  18857  ghmpreima  18866  ghmeql  18867  ghmnsgima  18868  ghmnsgpreima  18869  ghmeqker  18871  ghmf1o  18874  gass  18917  cntzmhm  18955  symgextres  19043  gsmsymgrfixlem1  19045  fvcosymgeq  19047  f1omvdconj  19064  pmtrfinv  19079  symgtrinv  19090  pmtr3ncomlem1  19091  sygbasnfpfi  19130  efginvrel2  19343  efgredleme  19359  ghmplusg  19457  prdscmnd  19472  gsumval3a  19514  gsumval3eu  19515  gsumzaddlem  19532  gsumzsplit  19538  gsumpt  19573  prdsgsum  19592  dprdfcntz  19628  dprdfadd  19633  dprdfeq0  19635  dprdf11  19636  dprdlub  19639  dprdspan  19640  dprd2dlem1  19654  dmdprdpr  19662  dprdpr  19663  dpjlem  19664  ablfac1eu  19686  prdsmulrcl  19860  prdsringd  19861  prdscrngd  19862  prds1  19863  rhmf1o  19986  rnrhmsubrg  20066  isabvd  20090  lmodfopnelem1  20169  lcomfsupp  20173  prdsvscacl  20240  prdslmodd  20241  lmhmco  20315  lmhmplusg  20316  lmhmvsca  20317  lmhmf1o  20318  lmhmeql  20327  lspextmo  20328  rrgsupp  20572  pjfo  20932  dsmmbas2  20954  dsmm0cl  20957  dsmmacl  20958  dsmmsubg  20960  dsmmlss  20961  frlmvplusgvalc  20984  frlmvscaval  20985  frlmplusgvalb  20986  frlmvscavalb  20987  frlmsslss2  20992  frlmphllem  20997  frlmphl  20998  frlmssuvc2  21012  frlmsslsp  21013  frlmup1  21015  frlmup2  21016  frlmup3  21017  frlmup4  21018  islindf4  21055  psrbagfsupp  21133  psrbaglesupp  21137  psrbaglesuppOLD  21138  psrbaglecl  21139  psrbagaddcl  21141  psrbagcon  21143  psrbagconOLD  21144  psrbaglefi  21145  psrbaglefiOLD  21146  psrbagconf1o  21149  psrbagconf1oOLD  21150  gsumbagdiaglemOLD  21151  gsumbagdiaglem  21154  psrass1lem  21156  psrvscaval  21171  psrlidm  21182  psrridm  21183  psrass1  21184  psrdi  21185  psrdir  21186  mplsubglem  21215  mplvscaval  21230  subrgmvrf  21245  mplbas2  21253  mvrf2  21278  mplind  21288  psrbagev1  21295  psrbagev1OLD  21296  psrbagev2  21297  evlslem3  21300  evlslem1  21302  evlsvar  21310  mpfind  21327  ismhp3  21343  mhpmulcl  21349  psrplusgpropd  21417  coe1add  21445  coe1addfv  21446  evl1addd  21517  evl1subd  21518  evl1muld  21519  pf1mpf  21528  pf1ind  21531  mamudir  21561  mamulid  21600  mamurid  21601  mdetrlin  21761  mdetrsca  21762  mdetralt  21767  mdetunilem7  21777  mdetunilem9  21779  madurid  21803  cnrest2  22447  lmss  22459  lmcnp  22465  cnt0  22507  cnt1  22511  cnhaus  22515  rncmp  22557  conncn  22587  2ndcomap  22619  1stccnp  22623  comppfsc  22693  1stckgenlem  22714  ptbasfi  22742  ptopn  22744  ptclsg  22776  ptcnp  22783  upxp  22784  txtube  22801  txcmplem1  22802  hauseqlcld  22807  xkohaus  22814  xkoptsub  22815  cnmpt11  22824  cnmpt21  22832  cnmpt22f  22836  cnmptcom  22839  qtopss  22876  qtopeu  22877  qtopomap  22879  qtopcmap  22880  kqffn  22886  hmeof1o2  22924  xkocnv  22975  rnelfm  23114  ptcmplem1  23213  cnextfres1  23229  ghmcnp  23276  tgphaus  23278  prdstmdd  23285  prdstgpd  23286  fmucnd  23454  psmetxrge0  23476  isxmet2d  23490  prdsmet  23533  blelrnps  23579  blelrn  23580  xmetresbl  23600  comet  23679  stdbdxmet  23681  met2ndci  23688  prdsxmslem2  23695  isngp3  23764  nmotri  23913  metdsre  24026  bndth  24131  evth  24132  fmcfil  24446  bcthlem4  24501  rrxcph  24566  rrxds  24567  rrxmet  24582  evthicc2  24634  ovolfsf  24645  ovolmge0  24651  ovollb2lem  24662  ovolunlem1a  24670  ovoliunlem1  24676  ovoliun  24679  ovoliun2  24680  ovolscalem1  24687  ovolicc1  24690  ovolicc2lem4  24694  ovolicc2  24696  voliunlem1  24724  voliunlem3  24726  volsup  24730  ioombl1lem2  24733  ioombl1lem4  24735  uniiccdif  24752  uniioombllem2  24757  uniioombllem3  24759  uniioombllem6  24762  volsup2  24779  vitalilem4  24785  mbfeqalem1  24815  mbfmulc2lem  24821  mbfmax  24823  mbfaddlem  24834  mbfadd  24835  mbfsub  24836  mbfsup  24838  mbfinf  24839  itg1ge0  24860  itg1addlem1  24866  i1faddlem  24867  i1fmullem  24868  i1fadd  24869  i1fmul  24870  itg1addlem4  24873  itg1addlem4OLD  24874  i1fmulclem  24877  i1fmulc  24878  itg1mulc  24879  i1fres  24880  itg10a  24885  itg1ge0a  24886  itg1lea  24887  mbfi1fseqlem3  24892  mbfi1fseqlem4  24893  mbfi1flimlem  24897  mbfmullem2  24899  mbfmul  24901  itg20  24912  itg2lea  24919  itg2splitlem  24923  itg2split  24924  itg2monolem1  24925  itg2monolem2  24926  itg2monolem3  24927  itg2mono  24928  itg2i1fseqle  24929  itg2i1fseq  24930  itg2addlem  24933  itg2gt0  24935  itg2cnlem1  24936  itg2cnlem2  24937  itg2cn  24938  itgitg1  24983  bddmulibl  25013  bddibl  25014  dvidlem  25089  dvaddbr  25112  dvmulbr  25113  dvaddf  25116  dvcmulf  25119  dvrec  25129  dvcnvlem  25150  rolle  25164  dveq0  25174  dv11cn  25175  dvivthlem2  25183  dvivth  25184  dvne0  25185  lhop1lem  25187  lhop1  25188  lhop2  25189  lhop  25190  ftc1cn  25217  tdeglem1  25230  tdeglem3  25232  tdeglem4  25234  tdeglem4OLD  25235  mdegleb  25239  mdegldg  25241  mdegaddle  25249  ply1remlem  25337  ply1rem  25338  fta1glem1  25340  fta1glem2  25341  fta1blem  25343  plyeq0lem  25381  plyeq0  25382  plyaddlem1  25384  coeeulem  25395  coeaddlem  25420  coemulc  25426  dgradd2  25439  dgrcolem2  25445  ofmulrt  25452  plyrem  25475  vieta1lem1  25480  vieta1  25482  plyexmo  25483  elqaalem3  25491  aannenlem1  25498  aalioulem2  25503  ulmuni  25561  ulmdvlem1  25569  ulmdv  25572  mbfulm  25575  iblulm  25576  itgulm  25577  rlimcnp2  26126  jensen  26148  amgm  26150  basellem3  26242  basellem7  26246  basellem9  26248  dchrelbas2  26395  dchrmulcl  26407  dchrfi  26413  dchreq  26416  dchrresb  26417  dchrinv  26419  dchr1re  26421  sumdchr2  26428  dchr2sum  26431  lgsqrlem2  26505  lgsqrlem3  26506  rpvmasum2  26670  dchrisum0re  26671  mirf1o  27040  lmif1o  27166  eqeefv  27281  axlowdimlem14  27333  vtxdgfisf  27853  2pthon3v  28316  nvinvfval  29010  sspg  29098  ssps  29100  sspmlem  29102  sspn  29106  lnon0  29168  ubthlem1  29240  pjfn  30079  kbpj  30326  kbass2  30487  elpjrn  30560  ofrn2  30985  off2  30986  ofresid  30987  xppreima2  30996  ofpreima2  31011  suppovss  31025  resf1o  31073  swrdrn3  31235  pwrssmgc  31286  mgcf1o  31289  gsumhashmul  31324  gsumle  31358  symgcom2  31361  pmtrcnel  31366  pmtrcnel2  31367  pmtrcnelor  31368  cycpmfvlem  31387  cycpmfv3  31390  cycpmcl  31391  cycpmco2rn  31400  cycpmco2  31408  cycpm3cl2  31411  cyc3co2  31415  cyc3evpm  31425  islinds5  31571  ellspds  31572  rhmpreimaidl  31611  elrspunidl  31614  rhmimaidl  31617  rhmpreimaprmidl  31635  dimkerim  31716  fedgmullem2  31719  fedgmul  31720  cmpcref  31808  rhmpreimacnlem  31842  fsumcvg4  31908  pl1cn  31913  qqhval2lem  31939  prodindf  31999  indpreima  32001  esumcvg  32062  ofcf  32079  ofcof  32083  measfn  32180  meascnbl  32195  sibfof  32315  sitgaddlemb  32323  subiwrdlen  32361  rrvfn  32420  plymul02  32533  signsplypnf  32537  signsply0  32538  reprsuc  32603  reprdifc  32615  breprexplema  32618  circlemethhgt  32631  hgt750lemb  32644  f1resrcmplf1dlem  33066  pthhashvtx  33097  cvmopnlem  33248  cvmliftmolem1  33251  cvmliftlem10  33264  cvmlift2lem9a  33273  cvmlift2lem6  33278  cvmlift2lem12  33284  cvmliftphtlem  33287  cvmlift3lem9  33297  mrsubrn  33483  elmrsubrn  33490  elmsubrn  33498  msubrn  33499  mclsind  33540  mclsppslem  33553  mclspps  33554  iprodefisumlem  33714  matunitlindflem1  35781  poimirlem1  35786  poimirlem2  35787  poimirlem3  35788  poimirlem16  35801  poimirlem17  35802  poimirlem19  35804  poimirlem20  35805  poimirlem22  35807  poimirlem23  35808  poimirlem29  35814  poimirlem30  35815  poimirlem31  35816  poimir  35818  mblfinlem2  35823  itg2addnclem3  35838  itg2addnc  35839  itg2gt0cn  35840  ftc1cnnc  35857  ftc1anclem5  35862  ftc1anclem7  35864  ftc1anc  35866  sdclem2  35908  istotbnd3  35937  sstotbnd2  35940  isbnd3  35950  heibor1lem  35975  rrnmet  35995  grpokerinj  36059  isdrngo2  36124  lfl1  37092  lfladdcl  37093  lflvscl  37099  lkr0f  37116  lkrsc  37119  eqlkr2  37122  eqlkr3  37123  ldualvaddval  37153  ldualvsval  37160  tendoeq1  38786  sticksstones1  40110  sticksstones2  40111  sticksstones3  40112  sticksstones12a  40121  sticksstones12  40122  metakunt19  40151  metakunt25  40157  metakunt33  40165  frlmvscadiccat  40245  frlmsnic  40271  pwspjmhmmgpd  40275  pwsgprod  40277  evlsbagval  40283  evlsaddval  40285  evlsmulval  40286  fsuppssind  40290  mhphf  40293  ismrcd1  40528  ismrcd2  40529  istopclsd  40530  isnacs3  40540  mzpaddmpt  40571  mzpmulmpt  40572  mzpsubst  40578  mzpcong  40802  fnwe2lem2  40884  islmodfg  40902  kercvrlsm  40916  dgrsub2  40968  mpaaeu  40983  rngunsnply  41006  idomrootle  41028  hausgraph  41045  fsovf1od  41605  brcoffn  41621  clsneiel1  41699  wfximgfd  41755  extoimad  41756  mnringmulrcld  41827  mnurndlem1  41880  caofcan  41922  ofmul12  41924  ofdivrec  41925  ofdivcan4  41926  ofdivdiv2  41927  dvconstbi  41933  binomcxplemnotnn0  41955  refsum2cnlem1  42561  ssmapsn  42737  preimaiocmnf  43080  fsumsupp0  43100  fsumsermpt  43101  climinf  43128  climinf2lem  43228  limsupmnflem  43242  limsupvaluz2  43260  supcnvlimsup  43262  limsupgtlem  43299  liminfvalxr  43305  liminflelimsupuz  43307  xlimconst2  43357  climxlim2  43368  icccncfext  43409  dvnprodlem1  43468  volicoff  43517  voliooicof  43518  fourierdlem25  43654  etransclem2  43758  etransclem35  43791  fge0iccico  43889  sge0tsms  43899  sge0sup  43910  sge0resrn  43923  sge0le  43926  sge0fodjrnlem  43935  sge0isum  43946  sge0seq  43965  nnfoctbdjlem  43974  meadjiunlem  43984  omeiunle  44036  hoicvr  44067  ovolval4lem1  44168  ovolval5lem3  44173  ovnovollem1  44175  ovnovollem2  44176  iinhoiicclem  44192  iunhoiioolem  44194  preimaicomnf  44227  smfresal  44300  smfsuplem1  44322  smflimsuplem2  44332  fcoreslem3  44537  fcoreslem4  44538  fcores  44539  mgmhmf1o  45319  resmgmhm2b  45332  mgmhmima  45334  mgmhmeql  45335  rnghmf1o  45439  ackvalsucsucval  46012  amgmwlem  46484