Theorem ffnd 6740

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

This proof depends on syntax axioms:   → wi 4   Fn wfn 6561  ⟶wf 6562

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-f 6570

This theorem is used by:  fnconstg  6800  f1fn  6809  fofn  6828  f1ofn  6855  feqmptd  6984  fssrescdmd  7159  fprb  7230  f1resrcmplf1dlem  7309  cocan1  7330  oprres  7620  off  7743  coof  7749  ofco  7750  caofref  7756  caofid0l  7758  caofid0r  7759  caofid1  7760  caofid2  7761  caofrss  7764  caoftrn  7766  fo2ndf  8169  fnwelem  8180  fnwe2lem3  8184  fnse  8187  suppsnop  8233  suppss  8249  suppssr  8250  suppssrg  8251  suppssof1  8254  suppofssd  8258  suppofss1d  8259  suppofss2d  8260  suppcoss  8262  smocdmdom  8414  elmapfn  8925  ralxpmap  8962  omxpenlem  9135  mapen  9198  f1finf1o  9302  unirnffid  9374  fdmfifsupp  9404  mapfien  9437  intrnfi  9445  marypha2  9468  ordtypelem7  9555  wemapsolem  9581  wemapso  9582  wemapso2lem  9583  unxpwdom2  9619  ixpiunwdom  9621  cantnfle  9709  cantnfp1lem2  9717  cantnfp1lem3  9718  cantnfp1  9719  oemapvali  9722  cantnflem1a  9723  cantnflem1c  9725  cantnflem3  9729  cantnf  9731  cnfcomlem  9737  cnfcom3  9742  updjudhcoinlf  10050  updjudhcoinrg  10051  fseqenlem1  10142  numacn  10167  infpwfien  10180  isf32lem2  10471  isf34lem7  10496  isf34lem6  10497  unirnfdomd  10691  ofsubeq0  12357  ofnegsub  12358  ofsubge0  12359  seqf1olem2  14225  resunimafz0  14631  wrdfn  14714  swrdvalfn  14842  swrdrn3  14844  pfxfn  14873  pfxid  14876  cats1un  14912  cshwfn  14994  ccatco  15028  limsupgle  15688  o1of2  15824  o1rlimmul  15830  isercolllem2  15877  isercoll  15879  isercoll2  15880  climsup  15881  fsumss  15935  ruclem11  16452  vdwlem2  17204  vdwlem6  17208  vdwlem9  17211  vdwlem12  17214  0ram  17242  ramub1lem1  17248  pwsle  17714  pwsleval  17715  pwsvscaval  17717  mrcuni  17845  mrcun  17846  invf1o  17994  funcres2c  18128  setcmon  18312  setcepi  18313  uncfcurf  18463  yoniso  18509  isacs4lem  18768  acsmapd  18778  chnso  18848  mgmn0plusgplusf  18878  gsumval2  18925  mgmhmf1o  18939  resmgmhm2b  18952  mgmhmima  18954  mgmhmeql  18955  prdsplusgsgrpcl  18971  prdssgrpd  18972  prdsplusgcl  19012  prdsidlem  19013  prdsmndd  19014  mhmf1o  19041  resmhm2b  19068  mhmimalem  19070  mhmima  19071  mhmeql  19072  prdspjmhm  19075  pwsco1mhm  19078  pwsco2mhm  19079  gsumwmhm  19091  frmdss2  19109  grpinvf1o  19269  prdsinvlem  19309  cycsubgcl  19471  ghmrn  19493  ghmpreima  19502  ghmeql  19503  ghmnsgima  19504  ghmnsgpreima  19505  ghmeqker  19507  ghmf1o  19512  ghmqusnsglem1  19545  ghmqusnsg  19547  ghmquskerlem1  19548  ghmquskerco  19549  ghmquskerlem3  19551  ghmqusker  19552  gass  19566  cntzmhm  19606  symgextres  19690  gsmsymgrfixlem1  19692  fvcosymgeq  19694  f1omvdconj  19711  pmtrfinv  19726  symgtrinv  19737  pmtr3ncomlem1  19738  sygbasnfpfi  19777  efginvrel2  19992  efgredleme  20008  ghmplusg  20111  prdscmnd  20126  gsumval3a  20168  gsumval3eu  20169  gsumzaddlem  20186  gsumzsplit  20192  gsumpt  20227  prdsgsum  20246  dprdfcntz  20282  dprdfadd  20287  dprdfeq0  20289  dprdf11  20290  dprdlub  20293  dprdspan  20294  dprd2dlem1  20308  dmdprdpr  20316  dprdpr  20317  dpjlem  20318  ablfac1eu  20340  gsumle  20410  prdsmulrngcl  20448  prdsrngd  20449  prdsringd  20601  prdscrngd  20602  prds1  20603  pwspjmhmmgpd  20608  pwsgprod  20610  rnghmf1o  20733  rhmf1o  20778  rhmimasubrnglem  20868  rnrhmsubrg  20908  rrgsupp  21004  imadrhmcl  21105  isabvd  21120  lmodfopnelem1  21224  lcomfsupp  21228  prdsvscacl  21294  prdslmodd  21295  lmhmco  21369  lmhmplusg  21370  lmhmvsca  21371  lmhmf1o  21372  lmhmeql  21381  lspextmo  21382  rhmpreimaidl  21622  rhmpreimaprmidl  21686  pjfo  22076  dsmmbas2  22098  dsmm0cl  22101  dsmmacl  22102  dsmmsubg  22104  dsmmlss  22105  frlmvplusgvalc  22128  frlmvscaval  22129  frlmplusgvalb  22130  frlmvscavalb  22131  frlmsslss2  22136  frlmphllem  22141  frlmphl  22142  frlmssuvc2  22156  frlmsslsp  22157  frlmup1  22159  frlmup2  22160  frlmup3  22161  frlmup4  22162  islindf4  22199  psrbagfsupp  22282  psrbaglesupp  22285  psrbaglecl  22286  psrbagaddcl  22287  psrbagcon  22288  psrbaglefi  22289  psrbagleadd1  22291  psrbagconf1o  22292  gsumbagdiaglem  22294  psrass1lem  22296  psrvscaval  22313  psrlidm  22324  psrridm  22325  psrass1  22326  psrdi  22327  psrdir  22328  psrascl  22341  mvrf2  22355  mplsubglem  22361  mplvscaval  22378  subrgmvrf  22398  mplbas2  22406  mplind  22434  psrbagev1  22441  psrbagev2  22442  evlslem3  22444  evlslem1  22446  evlsvvval  22457  evlsvar  22459  evladdval  22467  evlmulval  22468  mpfind  22479  mplmapghm  22486  evlsaddval  22493  evlsmulval  22494  selvvvval  22506  ismhp3  22518  mhpmulcl  22525  psdmplcl  22538  psdadd  22539  psdvsca  22540  psdmul  22542  psdmvr  22545  psrplusgpropd  22608  coe1add  22638  coe1addfv  22639  evl1addd  22714  evl1subd  22715  evl1muld  22716  pf1mpf  22725  pf1ind  22728  evls1fpws  22742  ressply1evl  22743  rhmply1vsca  22758  mamudir  22774  mamulid  22811  mamurid  22812  mdetrlin  22972  mdetrsca  22973  mdetralt  22978  mdetunilem7  22988  mdetunilem9  22990  madurid  23014  matunitlindflem1  23049  cnrest2  23659  lmss  23671  lmcnp  23677  cnt0  23719  cnt1  23723  cnhaus  23727  rncmp  23769  conncn  23799  2ndcomap  23832  1stccnp  23836  comppfsc  23906  1stckgenlem  23927  ptbasfi  23955  ptopn  23957  ptclsg  23989  ptcnp  23996  upxp  23997  txtube  24014  txcmplem1  24015  hauseqlcld  24020  xkohaus  24027  xkoptsub  24028  cnmpt11  24037  cnmpt21  24045  cnmpt22f  24049  cnmptcom  24052  qtopss  24089  qtopeu  24090  qtopomap  24092  qtopcmap  24093  kqffn  24099  hmeof1o2  24137  xkocnv  24188  rnelfm  24327  ptcmplem1  24426  cnextfres1  24442  ghmcnp  24489  tgphaus  24491  prdstmdd  24498  prdstgpd  24499  fmucnd  24665  psmetxrge0  24687  isxmet2d  24701  prdsmet  24744  blelrnps  24790  blelrn  24791  xmetresbl  24811  comet  24887  stdbdxmet  24889  met2ndci  24896  prdsxmslem2  24903  isngp3  24972  nmotri  25113  metdsre  25228  bndth  25334  evth  25335  fmcfil  25648  bcthlem4  25703  rrxcph  25768  rrxds  25769  rrxmet  25784  evthicc2  25836  ovolfsf  25847  ovolmge0  25853  ovollb2lem  25864  ovolunlem1a  25872  ovoliunlem1  25878  ovoliun  25881  ovoliun2  25882  ovolscalem1  25889  ovolicc1  25892  ovolicc2lem4  25896  ovolicc2  25898  voliunlem1  25926  voliunlem3  25928  volsup  25932  ioombl1lem2  25935  ioombl1lem4  25937  uniiccdif  25954  uniioombllem2  25959  uniioombllem3  25961  uniioombllem6  25964  volsup2  25981  vitalilem4  25987  mbfeqalem1  26017  mbfmulc2lem  26023  mbfmax  26025  mbfaddlem  26036  mbfadd  26037  mbfsub  26038  mbfsup  26040  mbfinf  26041  itg1ge0  26062  itg1addlem1  26068  i1faddlem  26069  i1fmullem  26070  i1fadd  26071  i1fmul  26072  itg1addlem4  26075  i1fmulclem  26078  i1fmulc  26079  itg1mulc  26080  i1fres  26081  itg10a  26086  itg1ge0a  26087  itg1lea  26088  mbfi1fseqlem3  26093  mbfi1fseqlem4  26094  mbfi1flimlem  26098  mbfmullem2  26100  mbfmul  26102  itg20  26113  itg2lea  26120  itg2splitlem  26124  itg2split  26125  itg2monolem1  26126  itg2monolem2  26127  itg2monolem3  26128  itg2mono  26129  itg2i1fseqle  26130  itg2i1fseq  26131  itg2addlem  26134  itg2gt0  26136  itg2cnlem1  26137  itg2cnlem2  26138  itg2cn  26139  itgitg1  26184  bddmulibl  26214  bddibl  26215  dvidlem  26290  dvaddbr  26313  dvmulbr  26314  dvaddf  26317  dvcmulf  26320  dvrec  26330  dvcnvlem  26351  rolle  26365  dveq0  26375  dv11cn  26376  dvivthlem2  26384  dvivth  26385  dvne0  26386  lhop1lem  26388  lhop1  26389  lhop2  26390  lhop  26391  ftc1cn  26418  tdeglem1  26431  tdeglem3  26432  tdeglem4  26433  mdegleb  26437  mdegldg  26439  mdegaddle  26447  ply1remlem  26538  ply1rem  26539  fta1glem1  26541  fta1glem2  26542  fta1blem  26544  idomrootle  26546  plyeq0lem  26584  plyeq0  26585  plyaddlem1  26587  coeeulem  26598  coeaddlem  26623  coemulc  26629  dgradd2  26642  dgrcolem2  26648  ofmulrt  26655  plymul02  26656  plyrem  26681  rnplynfin  26685  plyconz  26686  vieta1lem1  26688  vieta1  26690  plyexmo  26691  rngunsnply  26693  elqaalem3  26701  aannenlem1  26712  aalioulem2  26717  ulmuni  26776  ulmdvlem1  26784  ulmdv  26787  mbfulm  26790  iblulm  26791  itgulm  26792  rlimcnp2  27351  jensen  27373  amgm  27375  basellem3  27467  basellem7  27471  basellem9  27473  dchrelbas2  27621  dchrmulcl  27633  dchrfi  27639  dchreq  27642  dchrresb  27643  dchrinv  27645  dchr1re  27647  sumdchr2  27654  dchr2sum  27657  lgsqrlem2  27731  lgsqrlem3  27732  rpvmasum2  27896  dchrisum0re  27897  mirf1o  29198  lmif1o  29357  elcgrabasi  29432  eqeefv  29538  axlowdimlem14  29590  vtxdgfisf  30114  pthhashvtx  30372  2pthon3v  30589  nvinvfval  31299  sspg  31387  ssps  31389  sspmlem  31391  sspn  31395  lnon0  31457  ubthlem1  31529  pjfn  32368  kbpj  32615  kbass2  32776  elpjrn  32849  ofrn2  33332  off2  33333  ofresid  33334  xppreima2  33343  ofpreima2  33358  suppovss  33371  resf1o  33418  prodindf  33525  indpreima  33528  pwrssmgc  33660  mgcf1o  33663  gsumfs2d  33721  gsumhashmul  33727  symgcom2  33744  pmtrcnel  33749  pmtrcnel2  33750  pmtrcnelor  33751  cycpmfvlem  33772  cycpmfv3  33775  cycpmcl  33776  cycpmco2rn  33785  cycpmco2  33793  cycpm3cl2  33796  cyc3co2  33800  cyc3evpm  33810  elrgspnlem1  33902  elrgspnlem2  33903  elrgspnlem4  33905  elrgspnsubrunlem1  33907  elrgspnsubrunlem2  33908  edompidlem  33960  gsumind  34010  islinds5  34027  ellspds  34028  elrspunidl  34082  elrspunsn  34083  rhmimaidl  34086  rprmdvdsprod  34170  1arithidomlem2  34172  evls1fn  34195  ply1dg1rt  34215  ply1mulrtss  34217  ply1degltel  34229  ply1degleel  34230  ply1degltlss  34231  ply1gsumz  34234  ig1pmindeg  34237  r1pquslmic  34247  0mplrim  34257  mplasclco  34259  selvply1rhmlema  34261  selvply1rhmlemb  34262  selvply1rhmlem1  34263  selvply1rhmlem4  34266  selvply1rhm0  34269  extvfvcl  34279  mplmulmvr  34282  evlextv  34285  mplvrpmmhm  34289  mplvrpmrhm  34290  psrmonprod  34295  esplyfval0  34307  esplyfval2  34308  esplyfv1  34312  esplyfv  34313  esplyfval3  34315  esplyfvaln  34317  esplyind  34318  vieta  34323  exsslsb  34340  ply1degltdimlem  34365  ply1degltdim  34366  dimkerim  34370  fedgmullem2  34373  fedgmul  34374  lvecendof1f1o  34376  fldextrspunlsplem  34416  fldextrspunlsp  34417  irngss  34430  irngnzply1  34434  extdgfialglem2  34436  irngnminplynz  34455  2sqr3minply  34523  cos9thpiminply  34531  cmpcref  34593  rhmpreimacnlem  34627  fsumcvg4  34693  pl1cn  34698  qqhval2lem  34724  esumcvg  34829  ofcf  34846  ofcof  34850  measfn  34948  meascnbl  34963  sibfof  35083  sitgaddlemb  35091  subiwrdlen  35129  rrvfn  35188  signsplypnf  35290  signsply0  35291  reprsuc  35355  reprdifc  35367  breprexplema  35370  circlemethhgt  35383  hgt750lemb  35396  onprcf1acwevd  36088  cvmopnlem  36251  cvmliftmolem1  36254  cvmliftlem10  36267  cvmlift2lem9a  36276  cvmlift2lem6  36281  cvmlift2lem12  36287  cvmliftphtlem  36290  cvmlift3lem9  36300  mrsubrn  36486  elmrsubrn  36493  elmsubrn  36501  msubrn  36502  mclsind  36543  mclsppslem  36556  mclspps  36557  iprodefisumlem  36720  weiunfrlem  37467  mh-inf3f1  37544  poimirlem1  38807  poimirlem2  38808  poimirlem3  38809  poimirlem16  38822  poimirlem17  38823  poimirlem19  38825  poimirlem20  38826  poimirlem22  38828  poimirlem23  38829  poimirlem29  38835  poimirlem30  38836  poimirlem31  38837  poimir  38839  mblfinlem2  38844  itg2addnclem3  38859  itg2addnc  38860  itg2gt0cn  38861  ftc1cnnc  38878  ftc1anclem5  38883  ftc1anclem7  38885  ftc1anc  38887  sdclem2  38942  istotbnd3  38971  sstotbnd2  38974  isbnd3  38984  heibor1lem  39009  rrnmet  39029  grpokerinj  39093  isdrngo2  39158  lfl1  40393  lfladdcl  40394  lflvscl  40400  lkr0f  40417  lkrsc  40420  eqlkr2  40423  eqlkr3  40424  ldualvaddval  40454  ldualvsval  40461  tendoeq1  42087  zndvdchrrhm  43289  hashscontpow  43438  aks6d1c3  43439  aks6d1c2lem4  43443  aks6d1c2  43446  sticksstones1  43462  sticksstones2  43463  sticksstones3  43464  sticksstones12a  43473  sticksstones12  43474  aks6d1c6lem2  43487  aks6d1c6lem3  43488  aks6d1c6isolem1  43490  aks6d1c6isolem3  43492  aks6d1c6lem5  43493  aks6d1c7lem1  43496  unitscyglem1  43511  dvun  43676  frlmbasfn  43831  frlmvscadiccat  43839  fiabv  43866  frlmsnic  43870  evlselvlem  43882  evlselv  43883  fsuppssind  43887  mhphf  43891  ismrcd1  43975  ismrcd2  43976  istopclsd  43977  isnacs3  43987  mzpaddmpt  44018  mzpmulmpt  44019  mzpsubst  44025  mzpcong  44245  islmodfg  44337  kercvrlsm  44351  dgrsub2  44402  mpaaeu  44417  hausgraph  44468  ofoafg  44617  ofoafo  44619  ofoaid1  44621  ofoaid2  44622  naddcnff  44625  naddcnffn  44626  naddcnffo  44627  naddcnfcom  44629  naddcnfid1  44630  naddcnfass  44632  fsovf1od  45277  brcoffn  45291  clsneiel1  45369  wfximgfd  45424  extoimad  45425  mnringmulrcld  45487  mnurndlem1  45526  caofcan  45568  ofmul12  45570  ofdivrec  45571  ofdivcan4  45572  ofdivdiv2  45573  dvconstbi  45579  binomcxplemnotnn0  45601  relpmin  46206  refsum2cnlem1  46328  ssmapsn  46502  preimaiocmnf  46845  fsumsupp0  46863  fsumsermpt  46864  climinf  46891  climinf2lem  46989  limsupmnflem  47003  limsupvaluz2  47021  supcnvlimsup  47023  limsupgtlem  47060  liminfvalxr  47066  liminflelimsupuz  47068  xlimconst2  47118  climxlim2  47129  icccncfext  47170  dvnprodlem1  47229  volicoff  47278  voliooicof  47279  fourierdlem25  47415  fourierdlem48  47437  fourierdlem49  47438  etransclem2  47519  etransclem35  47552  fge0iccico  47653  sge0tsms  47663  sge0sup  47674  sge0resrn  47687  sge0le  47690  sge0fodjrnlem  47699  sge0isum  47710  sge0seq  47729  nnfoctbdjlem  47738  meadjiunlem  47748  omeiunle  47800  hoicvr  47831  ovolval4lem1  47932  ovolval5lem3  47937  ovnovollem1  47939  ovnovollem2  47940  iinhoiicclem  47956  iunhoiioolem  47958  preimaicomnf  47994  smfresal  48071  smfsuplem1  48094  smflimsuplem2  48104  tmachlem-franscan  48232  fcoreslem3  48408  fcoreslem4  48409  fcores  48410  isubgredg  49237  upgrimpths  49280  ackvalsucsucval  50131  funchomf  50544  imasubc  50598  imassc  50600  imaid  50601  prcofdiag1  50859  prcofdiag  50860  oppfdiag1  50880  oppfdiag  50882  crossp3d  51395  veroquadmodzerod  51412  amgmwlem  51415