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

Theorem ffnd 6508
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 6507 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 17 1 (𝜑𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 6343  wf 6344
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 6352
This theorem is referenced by:  fnconstg  6560  f1fn  6569  fofn  6585  f1ofn  6609  feqmptd  6726  fprb  6948  rnmptc  6961  cocan1  7038  oprres  7305  off  7413  ofco  7418  caofref  7424  caofid0l  7426  caofid0r  7427  caofid1  7428  caofid2  7429  caofrss  7431  caoftrn  7433  fo2ndf  7806  fnwelem  7814  fnse  7816  suppsnop  7833  suppss  7849  suppssr  7850  suppssof1  7852  suppofssd  7856  suppofss1d  7857  suppofss2d  7858  smorndom  7994  elmapfn  8418  ralxpmap  8448  omxpenlem  8606  mapen  8669  f1finf1o  8733  unirnffid  8804  fdmfifsupp  8831  mapfien  8859  intrnfi  8868  marypha2  8891  ordtypelem7  8976  wemapsolem  9002  wemapso  9003  wemapso2lem  9004  unxpwdom2  9040  ixpiunwdom  9043  cantnfle  9122  cantnfp1lem2  9130  cantnfp1lem3  9131  cantnfp1  9132  oemapvali  9135  cantnflem1a  9136  cantnflem1c  9138  cantnflem3  9142  cantnf  9144  cnfcomlem  9150  cnfcom3  9155  updjudhcoinlf  9349  updjudhcoinrg  9350  fseqenlem1  9438  numacn  9463  infpwfien  9476  isf32lem2  9764  isf34lem7  9789  isf34lem6  9790  unirnfdomd  9977  ofsubeq0  11623  ofnegsub  11624  ofsubge0  11625  seqf1olem2  13398  resunimafz0  13791  wrdfn  13864  swrdvalfn  14001  pfxfn  14031  pfxid  14034  cats1un  14071  cshwfn  14151  ccatco  14185  limsupgle  14822  o1of2  14957  o1rlimmul  14963  isercolllem2  15010  isercoll  15012  isercoll2  15013  climsup  15014  fsumss  15070  ruclem11  15581  vdwlem2  16306  vdwlem6  16310  vdwlem9  16313  vdwlem12  16316  0ram  16344  ramub1lem1  16350  pwsle  16753  pwsleval  16754  pwsvscaval  16756  mrcuni  16880  mrcun  16881  invf1o  17027  funcres2c  17159  setcmon  17335  setcepi  17336  uncfcurf  17477  yoniso  17523  isacs4lem  17766  acsmapd  17776  gsumval2  17884  prdsplusgcl  17930  prdsidlem  17931  prdsmndd  17932  mhmf1o  17954  resmhm2b  17975  mhmima  17977  mhmeql  17978  prdspjmhm  17981  pwsco1mhm  17984  pwsco2mhm  17985  gsumwmhm  17998  frmdss2  18016  grpinvf1o  18107  prdsinvlem  18146  cycsubgcl  18287  ghmrn  18309  ghmpreima  18318  ghmeql  18319  ghmnsgima  18320  ghmnsgpreima  18321  ghmeqker  18323  ghmf1o  18326  gass  18369  cntzmhm  18407  symgextres  18482  gsmsymgrfixlem1  18484  fvcosymgeq  18486  f1omvdconj  18503  pmtrfinv  18518  symgtrinv  18529  pmtr3ncomlem1  18530  sygbasnfpfi  18569  efginvrel2  18782  efgredleme  18798  ghmplusg  18895  prdscmnd  18910  gsumval3a  18952  gsumval3eu  18953  gsumzaddlem  18970  gsumzsplit  18976  gsumpt  19011  prdsgsum  19030  dprdfcntz  19066  dprdfadd  19071  dprdfeq0  19073  dprdf11  19074  dprdlub  19077  dprdspan  19078  dprd2dlem1  19092  dmdprdpr  19100  dprdpr  19101  dpjlem  19102  ablfac1eu  19124  prdsmulrcl  19290  prdsringd  19291  prdscrngd  19292  prds1  19293  rhmf1o  19413  rnrhmsubrg  19496  isabvd  19520  lmodfopnelem1  19599  lcomfsupp  19603  prdsvscacl  19669  prdslmodd  19670  lmhmco  19744  lmhmplusg  19745  lmhmvsca  19746  lmhmf1o  19747  lmhmeql  19756  lspextmo  19757  rrgsupp  19992  psrbaglesupp  20076  psrbagcon  20079  psrbaglefi  20080  psrbagconf1o  20082  gsumbagdiaglem  20083  psrvscaval  20100  psrlidm  20111  psrridm  20112  psrass1  20113  psrdi  20114  psrdir  20115  mplsubglem  20142  mplvscaval  20156  subrgmvrf  20171  mplbas2  20179  mvrf2  20200  mplind  20210  psrbagev1  20218  evlslem3  20221  evlslem1  20223  evlsvar  20231  mpfind  20248  mhpinvcl  20267  psrplusgpropd  20332  coe1add  20360  coe1addfv  20361  evl1addd  20432  evl1subd  20433  evl1muld  20434  pf1mpf  20443  pf1ind  20446  pjfo  20787  dsmmbas2  20809  dsmm0cl  20812  dsmmacl  20813  dsmmsubg  20815  dsmmlss  20816  frlmvplusgvalc  20839  frlmvscaval  20840  frlmplusgvalb  20841  frlmvscavalb  20842  frlmsslss2  20847  frlmphllem  20852  frlmphl  20853  frlmssuvc2  20867  frlmsslsp  20868  frlmup1  20870  frlmup2  20871  frlmup3  20872  frlmup4  20873  islindf4  20910  mamudir  20941  mamulid  20978  mamurid  20979  mdetrlin  21139  mdetrsca  21140  mdetralt  21145  mdetunilem7  21155  mdetunilem9  21157  madurid  21181  cnrest2  21822  lmss  21834  lmcnp  21840  cnt0  21882  cnt1  21886  cnhaus  21890  rncmp  21932  conncn  21962  2ndcomap  21994  1stccnp  21998  comppfsc  22068  1stckgenlem  22089  ptbasfi  22117  ptopn  22119  ptclsg  22151  ptcnp  22158  upxp  22159  txtube  22176  txcmplem1  22177  hauseqlcld  22182  xkohaus  22189  xkoptsub  22190  cnmpt11  22199  cnmpt21  22207  cnmpt22f  22211  cnmptcom  22214  qtopss  22251  qtopeu  22252  qtopomap  22254  qtopcmap  22255  kqffn  22261  hmeof1o2  22299  xkocnv  22350  rnelfm  22489  ptcmplem1  22588  cnextfres1  22604  ghmcnp  22650  tgphaus  22652  prdstmdd  22659  prdstgpd  22660  fmucnd  22828  psmetxrge0  22850  isxmet2d  22864  prdsmet  22907  blelrnps  22953  blelrn  22954  xmetresbl  22974  comet  23050  stdbdxmet  23052  met2ndci  23059  prdsxmslem2  23066  isngp3  23134  nmotri  23275  metdsre  23388  bndth  23489  evth  23490  fmcfil  23802  bcthlem4  23857  rrxcph  23922  rrxds  23923  rrxmet  23938  evthicc2  23988  ovolfsf  23999  ovolmge0  24005  ovollb2lem  24016  ovolunlem1a  24024  ovoliunlem1  24030  ovoliun  24033  ovoliun2  24034  ovolscalem1  24041  ovolicc1  24044  ovolicc2lem4  24048  ovolicc2  24050  voliunlem1  24078  voliunlem3  24080  volsup  24084  ioombl1lem2  24087  ioombl1lem4  24089  uniiccdif  24106  uniioombllem2  24111  uniioombllem3  24113  uniioombllem6  24116  volsup2  24133  vitalilem4  24139  mbfeqalem1  24169  mbfmulc2lem  24175  mbfmax  24177  mbfaddlem  24188  mbfadd  24189  mbfsub  24190  mbfsup  24192  mbfinf  24193  itg1ge0  24214  itg1addlem1  24220  i1faddlem  24221  i1fmullem  24222  i1fadd  24223  i1fmul  24224  itg1addlem4  24227  i1fmulclem  24230  i1fmulc  24231  itg1mulc  24232  i1fres  24233  itg10a  24238  itg1ge0a  24239  itg1lea  24240  mbfi1fseqlem3  24245  mbfi1fseqlem4  24246  mbfi1flimlem  24250  mbfmullem2  24252  mbfmul  24254  itg20  24265  itg2lea  24272  itg2splitlem  24276  itg2split  24277  itg2monolem1  24278  itg2monolem2  24279  itg2monolem3  24280  itg2mono  24281  itg2i1fseqle  24282  itg2i1fseq  24283  itg2addlem  24286  itg2gt0  24288  itg2cnlem1  24289  itg2cnlem2  24290  itg2cn  24291  itgitg1  24336  bddmulibl  24366  bddibl  24367  dvidlem  24440  dvaddbr  24462  dvmulbr  24463  dvaddf  24466  dvcmulf  24469  dvrec  24479  dvcnvlem  24500  rolle  24514  dveq0  24524  dv11cn  24525  dvivthlem2  24533  dvivth  24534  dvne0  24535  lhop1lem  24537  lhop1  24538  lhop2  24539  lhop  24540  ftc1cn  24567  tdeglem4  24581  mdegleb  24585  mdegldg  24587  mdegaddle  24595  ply1remlem  24683  ply1rem  24684  fta1glem1  24686  fta1glem2  24687  fta1blem  24689  plyeq0lem  24727  plyeq0  24728  plyaddlem1  24730  coeeulem  24741  coeaddlem  24766  coemulc  24772  dgradd2  24785  dgrcolem2  24791  ofmulrt  24798  plyrem  24821  vieta1lem1  24826  vieta1  24828  plyexmo  24829  elqaalem3  24837  aannenlem1  24844  aalioulem2  24849  ulmuni  24907  ulmdvlem1  24915  ulmdv  24918  mbfulm  24921  iblulm  24922  itgulm  24923  rlimcnp2  25471  jensen  25493  amgm  25495  basellem3  25587  basellem7  25591  basellem9  25593  dchrelbas2  25740  dchrmulcl  25752  dchrfi  25758  dchreq  25761  dchrresb  25762  dchrinv  25764  dchr1re  25766  sumdchr2  25773  dchr2sum  25776  lgsqrlem2  25850  lgsqrlem3  25851  rpvmasum2  26015  dchrisum0re  26016  mirf1o  26382  lmif1o  26508  eqeefv  26616  axlowdimlem14  26668  vtxdgfisf  27185  2pthon3v  27649  nvinvfval  28344  sspg  28432  ssps  28434  sspmlem  28436  sspn  28440  lnon0  28502  ubthlem1  28574  pjfn  29413  kbpj  29660  kbass2  29821  elpjrn  29894  ofrn2  30315  off2  30316  ofresid  30317  xppreima2  30323  ofpreima2  30339  suppovss  30354  resf1o  30392  swrdrn3  30556  gsumle  30652  symgcom2  30655  pmtrcnel  30660  pmtrcnel2  30661  pmtrcnelor  30662  cycpmfvlem  30681  cycpmfv3  30684  cycpmcl  30685  cycpmco2rn  30694  cycpmco2  30702  cycpm3cl2  30705  cyc3co2  30709  cyc3evpm  30719  islinds5  30859  ellspds  30860  dimkerim  30922  fedgmullem2  30925  fedgmul  30926  cmpcref  31013  fsumcvg4  31092  pl1cn  31097  qqhval2lem  31121  prodindf  31181  indpreima  31183  esumcvg  31244  ofcf  31261  ofcof  31265  measfn  31362  meascnbl  31377  sibfof  31497  sitgaddlemb  31505  subiwrdlen  31543  rrvfn  31602  plymul02  31715  signsplypnf  31719  signsply0  31720  reprsuc  31785  reprdifc  31797  breprexplema  31800  circlemethhgt  31813  hgt750lemb  31826  f1resrcmplf1dlem  32256  pthhashvtx  32271  cvmopnlem  32422  cvmliftmolem1  32425  cvmliftlem10  32438  cvmlift2lem9a  32447  cvmlift2lem6  32452  cvmlift2lem12  32458  cvmliftphtlem  32461  cvmlift3lem9  32471  mrsubrn  32657  elmrsubrn  32664  elmsubrn  32672  msubrn  32673  mclsind  32714  mclsppslem  32727  mclspps  32728  iprodefisumlem  32869  matunitlindflem1  34769  poimirlem1  34774  poimirlem2  34775  poimirlem3  34776  poimirlem16  34789  poimirlem17  34790  poimirlem19  34792  poimirlem20  34793  poimirlem22  34795  poimirlem23  34796  poimirlem29  34802  poimirlem30  34803  poimirlem31  34804  poimir  34806  mblfinlem2  34811  itg2addnclem3  34826  itg2addnc  34827  itg2gt0cn  34828  ftc1cnnc  34847  ftc1anclem5  34852  ftc1anclem7  34854  ftc1anc  34856  sdclem2  34898  istotbnd3  34930  sstotbnd2  34933  isbnd3  34943  heibor1lem  34968  rrnmet  34988  grpokerinj  35052  isdrngo2  35117  lfl1  36086  lfladdcl  36087  lflvscl  36093  lkr0f  36110  lkrsc  36113  eqlkr2  36116  eqlkr3  36117  ldualvaddval  36147  ldualvsval  36154  tendoeq1  37780  frlmvscadiccat  39023  frlmsnic  39027  ismrcd1  39173  ismrcd2  39174  istopclsd  39175  isnacs3  39185  mzpaddmpt  39216  mzpmulmpt  39217  mzpsubst  39223  mzpcong  39447  fnwe2lem2  39529  islmodfg  39547  kercvrlsm  39561  dgrsub2  39613  mpaaeu  39628  rngunsnply  39651  idomrootle  39673  hausgraph  39690  fsovf1od  40240  brcoffn  40258  clsneiel1  40336  wfximgfd  40392  extoimad  40393  mnurndlem1  40494  caofcan  40532  ofmul12  40534  ofdivrec  40535  ofdivcan4  40536  ofdivdiv2  40537  dvconstbi  40543  binomcxplemnotnn0  40565  refsum2cnlem1  41171  ssmapsn  41355  preimaiocmnf  41713  fsumsupp0  41735  fsumsermpt  41736  climinf  41763  climinf2lem  41863  limsupmnflem  41877  limsupvaluz2  41895  supcnvlimsup  41897  limsupgtlem  41934  liminfvalxr  41940  liminflelimsupuz  41942  xlimconst2  41992  climxlim2  42003  icccncfext  42046  dvnprodlem1  42107  volicoff  42157  voliooicof  42158  fourierdlem25  42294  etransclem2  42398  etransclem35  42431  fge0iccico  42529  sge0tsms  42539  sge0sup  42550  sge0resrn  42563  sge0le  42566  sge0fodjrnlem  42575  sge0isum  42586  sge0seq  42605  nnfoctbdjlem  42614  meadjiunlem  42624  omeiunle  42676  hoicvr  42707  ovolval4lem1  42808  ovolval5lem3  42813  ovnovollem1  42815  ovnovollem2  42816  iinhoiicclem  42832  iunhoiioolem  42834  preimaicomnf  42867  smfresal  42940  smfsuplem1  42962  smflimsuplem2  42972  mgmhmf1o  43931  resmgmhm2b  43944  mgmhmima  43946  mgmhmeql  43947  rnghmf1o  44102  amgmwlem  44831
  Copyright terms: Public domain W3C validator