MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ffnd Structured version   Visualization version   GIF version

Theorem ffnd 6224
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
StepHypRef Expression
1 ffnd.1 . 2 (𝜑𝐹:𝐴𝐵)
2 ffn 6223 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 17 1 (𝜑𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 6063  wf 6064
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 198  df-an 385  df-f 6072
This theorem is referenced by:  fnconstg  6275  f1fn  6284  fofn  6300  f1ofn  6321  feqmptd  6438  cocan1  6738  oprres  7000  off  7110  ofco  7115  caofref  7121  caofid0l  7123  caofid0r  7124  caofid1  7125  caofid2  7126  caofrss  7128  caoftrn  7130  fo2ndf  7486  fnwelem  7494  fnse  7496  suppss  7528  suppssr  7529  suppssof1  7531  suppofss1d  7535  suppofss2d  7536  smorndom  7669  elmapfn  8083  ralxpmap  8112  omxpenlem  8268  mapen  8331  f1finf1o  8394  unirnffid  8465  fdmfifsupp  8492  mapfien  8520  intrnfi  8529  marypha2  8552  ordtypelem7  8636  wemapsolem  8662  wemapso  8663  wemapso2lem  8664  unxpwdom2  8700  ixpiunwdom  8703  cantnfle  8783  cantnfp1lem2  8791  cantnfp1lem3  8792  cantnfp1  8793  oemapvali  8796  cantnflem1a  8797  cantnflem1c  8799  cantnflem3  8803  cantnf  8805  cnfcomlem  8811  cnfcom3  8816  updjudhcoinlf  9009  updjudhcoinrg  9010  fseqenlem1  9098  numacn  9123  isf32lem2  9429  isf34lem7  9454  isf34lem6  9455  unirnfdomd  9642  ofsubeq0  11271  ofnegsub  11272  ofsubge0  11273  seqf1olem2  13048  resunimafz0  13430  wrdfn  13500  swrdvalfn  13628  swrdidOLD  13630  swrdccat1OLD  13659  swrdccat2  13660  pfxfn  13670  pfxid  13673  cats1un  13719  cshwfn  13830  ccatco  13864  limsupgle  14493  o1of2  14628  o1rlimmul  14634  isercolllem2  14681  isercoll  14683  isercoll2  14684  climsup  14685  fsumss  14741  ruclem11  15251  vdwlem2  15965  vdwlem6  15969  vdwlem9  15972  vdwlem12  15975  0ram  16003  ramub1lem1  16009  pwsle  16418  pwsleval  16419  pwsvscaval  16421  mrcuni  16547  mrcun  16548  invf1o  16694  funcres2c  16826  setcmon  17002  setcepi  17003  uncfcurf  17145  yoniso  17191  isacs4lem  17434  acsmapd  17444  gsumval2  17546  prdsplusgcl  17587  prdsidlem  17588  prdsmndd  17589  mhmf1o  17611  resmhm2b  17627  mhmima  17629  mhmeql  17630  prdspjmhm  17633  pwsco1mhm  17636  pwsco2mhm  17637  gsumwmhm  17649  frmdss2  17667  grpinvf1o  17752  prdsinvlem  17791  cycsubgcl  17884  ghmrn  17937  ghmpreima  17946  ghmeql  17947  ghmnsgima  17948  ghmnsgpreima  17949  ghmeqker  17951  ghmf1o  17954  gass  17997  cntzmhm  18034  symgextres  18108  gsmsymgrfixlem1  18110  fvcosymgeq  18112  f1omvdconj  18129  pmtrfinv  18144  symgtrinv  18155  pmtr3ncomlem1  18156  sygbasnfpfi  18196  efgredleme  18421  ghmplusg  18515  prdscmnd  18530  gsumval3a  18570  gsumval3eu  18571  gsumzaddlem  18587  gsumzsplit  18593  gsumpt  18627  prdsgsum  18643  dprdfcntz  18681  dprdfadd  18686  dprdfeq0  18688  dprdf11  18689  dprdlub  18692  dprdspan  18693  dprd2dlem1  18707  dmdprdpr  18715  dprdpr  18716  dpjlem  18717  ablfac1eu  18739  prdsmulrcl  18878  prdsringd  18879  prdscrngd  18880  prds1  18881  rhmf1o  19001  isabvd  19089  lmodfopnelem1  19168  lcomfsupp  19172  prdsvscacl  19240  prdslmodd  19241  lmhmco  19315  lmhmplusg  19316  lmhmvsca  19317  lmhmf1o  19318  lmhmeql  19327  lspextmo  19328  rrgsupp  19565  psrbaglesupp  19642  psrbagcon  19645  psrbaglefi  19646  psrbagconf1o  19648  gsumbagdiaglem  19649  psrvscaval  19666  psrlidm  19677  psrridm  19678  psrass1  19679  psrdi  19680  psrdir  19681  mplsubglem  19708  mplvscaval  19722  subrgmvrf  19736  mplbas2  19744  mvrf2  19765  mplind  19775  psrbagev1  19783  evlslem3  19787  evlslem1  19788  evlsvar  19796  mpfind  19809  psrplusgpropd  19879  coe1add  19907  coe1addfv  19908  evl1addd  19978  evl1subd  19979  evl1muld  19980  pf1mpf  19989  pf1ind  19992  pjfo  20335  dsmmbas2  20357  dsmm0cl  20360  dsmmacl  20361  dsmmsubg  20363  dsmmlss  20364  frlmvscaval  20386  frlmsslss2  20390  frlmphllem  20395  frlmphl  20396  frlmssuvc2  20410  frlmsslsp  20411  frlmup1  20413  frlmup2  20414  frlmup3  20415  frlmup4  20416  islindf4  20453  mamudir  20486  mamulid  20523  mamurid  20524  mdetrlin  20685  mdetrsca  20686  mdetralt  20691  mdetunilem7  20701  mdetunilem9  20703  madurid  20727  cnrest2  21370  lmss  21382  lmcnp  21388  cnt0  21430  cnt1  21434  cnhaus  21438  rncmp  21479  conncn  21509  2ndcomap  21541  1stccnp  21545  comppfsc  21615  1stckgenlem  21636  ptbasfi  21664  ptopn  21666  ptclsg  21698  ptcnp  21705  upxp  21706  txtube  21723  txcmplem1  21724  hauseqlcld  21729  xkohaus  21736  xkoptsub  21737  cnmpt11  21746  cnmpt21  21754  cnmpt22f  21758  cnmptcom  21761  qtopss  21798  qtopeu  21799  qtopomap  21801  qtopcmap  21802  kqffn  21808  hmeof1o2  21846  xkocnv  21897  rnelfm  22036  ptcmplem1  22135  cnextfres1  22151  ghmcnp  22197  tgphaus  22199  prdstmdd  22206  prdstgpd  22207  fmucnd  22375  psmetxrge0  22397  isxmet2d  22411  prdsmet  22454  blelrnps  22500  blelrn  22501  xmetresbl  22521  comet  22597  stdbdxmet  22599  met2ndci  22606  prdsxmslem2  22613  isngp3  22681  nmotri  22822  metdsre  22935  bndth  23036  evth  23037  fmcfil  23349  bcthlem4  23404  rrxcph  23469  rrxds  23470  rrxmet  23480  evthicc2  23518  ovolfsf  23529  ovolmge0  23535  ovollb2lem  23546  ovolunlem1a  23554  ovoliunlem1  23560  ovoliun  23563  ovoliun2  23564  ovolscalem1  23571  ovolicc1  23574  ovolicc2lem4  23578  ovolicc2  23580  voliunlem1  23608  voliunlem3  23610  volsup  23614  ioombl1lem2  23617  ioombl1lem4  23619  uniiccdif  23636  uniioombllem2  23641  uniioombllem3  23643  uniioombllem6  23646  volsup2  23663  vitalilem4  23669  mbfeqalem1  23699  mbfmulc2lem  23705  mbfmax  23707  mbfaddlem  23718  mbfadd  23719  mbfsub  23720  mbfsup  23722  mbfinf  23723  itg1ge0  23744  itg1addlem1  23750  i1faddlem  23751  i1fmullem  23752  i1fadd  23753  i1fmul  23754  itg1addlem4  23757  i1fmulclem  23760  i1fmulc  23761  itg1mulc  23762  i1fres  23763  itg10a  23768  itg1ge0a  23769  itg1lea  23770  mbfi1fseqlem3  23775  mbfi1fseqlem4  23776  mbfi1flimlem  23780  mbfmullem2  23782  mbfmul  23784  itg20  23795  itg2lea  23802  itg2splitlem  23806  itg2split  23807  itg2monolem1  23808  itg2monolem2  23809  itg2monolem3  23810  itg2mono  23811  itg2i1fseqle  23812  itg2i1fseq  23813  itg2addlem  23816  itg2gt0  23818  itg2cnlem1  23819  itg2cnlem2  23820  itg2cn  23821  itgitg1  23866  bddmulibl  23896  bddibl  23897  dvidlem  23970  dvaddbr  23992  dvmulbr  23993  dvaddf  23996  dvcmulf  23999  dvrec  24009  dvcnvlem  24030  rolle  24044  dveq0  24054  dv11cn  24055  dvivthlem2  24063  dvivth  24064  dvne0  24065  lhop1lem  24067  lhop1  24068  lhop2  24069  lhop  24070  ftc1cn  24097  tdeglem4  24111  mdegleb  24115  mdegldg  24117  mdegaddle  24125  ply1remlem  24213  ply1rem  24214  fta1glem1  24216  fta1glem2  24217  fta1blem  24219  plyeq0lem  24257  plyeq0  24258  plyaddlem1  24260  coeeulem  24271  coeaddlem  24296  coemulc  24302  dgradd2  24315  dgrcolem2  24321  ofmulrt  24328  plyrem  24351  vieta1lem1  24356  vieta1  24358  elqaalem3  24367  aannenlem1  24374  aalioulem2  24379  ulmuni  24437  ulmdvlem1  24445  ulmdv  24448  mbfulm  24451  iblulm  24452  itgulm  24453  rlimcnp2  24984  jensen  25006  amgm  25008  basellem3  25100  basellem7  25104  basellem9  25106  dchrelbas2  25253  dchrmulcl  25265  dchrfi  25271  dchreq  25274  dchrresb  25275  dchrinv  25277  dchr1re  25279  sumdchr2  25286  dchr2sum  25289  lgsqrlem2  25363  lgsqrlem3  25364  rpvmasum2  25492  dchrisum0re  25493  mirf1o  25855  lmif1o  25978  eqeefv  26074  axlowdimlem14  26126  vtxdgfisf  26663  2pthon3v  27166  nvinvfval  27951  sspg  28039  ssps  28041  sspmlem  28043  sspn  28047  lnon0  28109  ubthlem1  28182  pjfn  29024  kbpj  29271  kbass2  29432  elpjrn  29505  ofrn2  29892  off2  29893  ofresid  29894  xppreima2  29900  ofpreima2  29916  resf1o  29954  gsumle  30226  cmpcref  30364  fsumcvg4  30443  pl1cn  30448  qqhval2lem  30472  prodindf  30532  indpreima  30534  esumcvg  30595  ofcf  30612  ofcof  30616  measfn  30714  meascnbl  30729  sibfof  30849  sitgaddlemb  30857  subiwrdlen  30895  rrvfn  30955  plymul02  31072  signsplypnf  31076  signsply0  31077  reprsuc  31144  reprdifc  31156  breprexplema  31159  circlemethhgt  31172  hgt750lemb  31185  cvmopnlem  31708  cvmliftmolem1  31711  cvmliftlem10  31724  cvmlift2lem9a  31733  cvmlift2lem6  31738  cvmlift2lem12  31744  cvmliftphtlem  31747  cvmlift3lem9  31757  mrsubrn  31858  elmrsubrn  31865  elmsubrn  31873  msubrn  31874  mclsind  31915  mclsppslem  31928  mclspps  31929  iprodefisumlem  32071  fprb  32114  matunitlindflem1  33829  poimirlem1  33834  poimirlem2  33835  poimirlem3  33836  poimirlem16  33849  poimirlem17  33850  poimirlem19  33852  poimirlem20  33853  poimirlem22  33855  poimirlem23  33856  poimirlem29  33862  poimirlem30  33863  poimirlem31  33864  poimir  33866  mblfinlem2  33871  itg2addnclem3  33886  itg2addnc  33887  itg2gt0cn  33888  ftc1cnnc  33907  ftc1anclem5  33912  ftc1anclem7  33914  ftc1anc  33916  sdclem2  33960  istotbnd3  33992  sstotbnd2  33995  isbnd3  34005  heibor1lem  34030  rrnmet  34050  grpokerinj  34114  isdrngo2  34179  lfl1  35026  lfladdcl  35027  lflvscl  35033  lkr0f  35050  lkrsc  35053  eqlkr2  35056  eqlkr3  35057  ldualvaddval  35087  ldualvsval  35094  tendoeq1  36720  ismrcd1  37939  ismrcd2  37940  istopclsd  37941  isnacs3  37951  mzpaddmpt  37982  mzpmulmpt  37983  mzpsubst  37989  mzpcong  38216  fnwe2lem2  38298  islmodfg  38316  kercvrlsm  38330  dgrsub2  38382  mpaaeu  38397  rngunsnply  38420  idomrootle  38450  hausgraph  38467  fsovf1od  38984  brcoffn  39002  clsneiel1  39080  wfximgfd  39137  extoimad  39138  caofcan  39196  ofmul12  39198  ofdivrec  39199  ofdivcan4  39200  ofdivdiv2  39201  dvconstbi  39207  binomcxplemnotnn0  39229  refsum2cnlem1  39848  rnmptc  40000  ssmapsn  40053  preimaiocmnf  40426  fsumsupp0  40448  fsumsermpt  40449  climinf  40476  climinf2lem  40576  limsupmnflem  40590  limsupvaluz2  40608  supcnvlimsup  40610  limsupgtlem  40647  liminfvalxr  40653  liminflelimsupuz  40655  xlimconst2  40699  climxlim2  40710  icccncfext  40738  dvnprodlem1  40799  volicoff  40849  voliooicof  40850  fourierdlem25  40986  etransclem2  41090  etransclem35  41123  fge0iccico  41224  sge0tsms  41234  sge0sup  41245  sge0resrn  41258  sge0le  41261  sge0fodjrnlem  41270  sge0isum  41281  sge0seq  41300  nnfoctbdjlem  41309  meadjiunlem  41319  omeiunle  41371  hoicvr  41402  ovolval4lem1  41503  ovolval5lem3  41508  ovnovollem1  41510  ovnovollem2  41511  iinhoiicclem  41527  iunhoiioolem  41529  preimaicomnf  41562  smfresal  41635  smfsuplem1  41657  smflimsuplem2  41667  mgmhmf1o  42456  resmgmhm2b  42469  mgmhmima  42471  mgmhmeql  42472  rnghmf1o  42572  amgmwlem  43220
  Copyright terms: Public domain W3C validator