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

Theorem ffnd 6670
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 6669 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 17 1 (𝜑𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 6492  wf 6493
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 398  df-f 6501
This theorem is referenced by:  fnconstg  6731  f1fn  6740  fofn  6759  f1ofn  6786  feqmptd  6911  fprb  7144  rnmptcOLD  7158  cocan1  7238  oprres  7523  off  7636  ofco  7641  caofref  7647  caofid0l  7649  caofid0r  7650  caofid1  7651  caofid2  7652  caofrss  7654  caoftrn  7656  fo2ndf  8054  fnwelem  8064  fnse  8066  suppsnop  8110  suppss  8126  suppssOLD  8127  suppssr  8128  suppssrg  8129  suppssof1  8131  suppofssd  8135  suppofss1d  8136  suppofss2d  8137  suppcoss  8139  smocdmdom  8315  elmapfn  8804  ralxpmap  8835  omxpenlem  9018  mapen  9086  f1finf1o  9216  f1finf1oOLD  9217  unirnffid  9289  fdmfifsupp  9316  mapfien  9345  intrnfi  9353  marypha2  9376  ordtypelem7  9461  wemapsolem  9487  wemapso  9488  wemapso2lem  9489  unxpwdom2  9525  ixpiunwdom  9527  cantnfle  9608  cantnfp1lem2  9616  cantnfp1lem3  9617  cantnfp1  9618  oemapvali  9621  cantnflem1a  9622  cantnflem1c  9624  cantnflem3  9628  cantnf  9630  cnfcomlem  9636  cnfcom3  9641  updjudhcoinlf  9869  updjudhcoinrg  9870  fseqenlem1  9961  numacn  9986  infpwfien  9999  isf32lem2  10291  isf34lem7  10316  isf34lem6  10317  unirnfdomd  10504  ofsubeq0  12151  ofnegsub  12152  ofsubge0  12153  seqf1olem2  13949  resunimafz0  14343  wrdfn  14417  swrdvalfn  14540  pfxfn  14570  pfxid  14573  cats1un  14610  cshwfn  14690  ccatco  14725  limsupgle  15360  o1of2  15496  o1rlimmul  15502  isercolllem2  15551  isercoll  15553  isercoll2  15554  climsup  15555  fsumss  15611  ruclem11  16123  vdwlem2  16855  vdwlem6  16859  vdwlem9  16862  vdwlem12  16865  0ram  16893  ramub1lem1  16899  pwsle  17375  pwsleval  17376  pwsvscaval  17378  mrcuni  17502  mrcun  17503  invf1o  17653  funcres2c  17789  setcmon  17974  setcepi  17975  uncfcurf  18129  yoniso  18175  isacs4lem  18434  acsmapd  18444  gsumval2  18542  prdsplusgcl  18588  prdsidlem  18589  prdsmndd  18590  mhmf1o  18613  resmhm2b  18634  mhmima  18636  mhmeql  18637  prdspjmhm  18640  pwsco1mhm  18643  pwsco2mhm  18644  gsumwmhm  18656  frmdss2  18674  grpinvf1o  18818  prdsinvlem  18857  cycsubgcl  19000  ghmrn  19022  ghmpreima  19031  ghmeql  19032  ghmnsgima  19033  ghmnsgpreima  19034  ghmeqker  19036  ghmf1o  19039  gass  19082  cntzmhm  19120  symgextres  19208  gsmsymgrfixlem1  19210  fvcosymgeq  19212  f1omvdconj  19229  pmtrfinv  19244  symgtrinv  19255  pmtr3ncomlem1  19256  sygbasnfpfi  19295  efginvrel2  19510  efgredleme  19526  ghmplusg  19625  prdscmnd  19640  gsumval3a  19681  gsumval3eu  19682  gsumzaddlem  19699  gsumzsplit  19705  gsumpt  19740  prdsgsum  19759  dprdfcntz  19795  dprdfadd  19800  dprdfeq0  19802  dprdf11  19803  dprdlub  19806  dprdspan  19807  dprd2dlem1  19821  dmdprdpr  19829  dprdpr  19830  dpjlem  19831  ablfac1eu  19853  prdsmulrcl  20036  prdsringd  20037  prdscrngd  20038  prds1  20039  pwspjmhmmgpd  20044  rhmf1o  20165  rnrhmsubrg  20257  isabvd  20282  lmodfopnelem1  20361  lcomfsupp  20365  prdsvscacl  20432  prdslmodd  20433  lmhmco  20507  lmhmplusg  20508  lmhmvsca  20509  lmhmf1o  20510  lmhmeql  20519  lspextmo  20520  rrgsupp  20764  pjfo  21124  dsmmbas2  21146  dsmm0cl  21149  dsmmacl  21150  dsmmsubg  21152  dsmmlss  21153  frlmvplusgvalc  21176  frlmvscaval  21177  frlmplusgvalb  21178  frlmvscavalb  21179  frlmsslss2  21184  frlmphllem  21189  frlmphl  21190  frlmssuvc2  21204  frlmsslsp  21205  frlmup1  21207  frlmup2  21208  frlmup3  21209  frlmup4  21210  islindf4  21247  psrbagfsupp  21325  psrbaglesupp  21329  psrbaglesuppOLD  21330  psrbaglecl  21331  psrbagaddcl  21333  psrbagcon  21335  psrbagconOLD  21336  psrbaglefi  21337  psrbaglefiOLD  21338  psrbagconf1o  21341  psrbagconf1oOLD  21342  gsumbagdiaglemOLD  21343  gsumbagdiaglem  21346  psrass1lem  21348  psrvscaval  21363  psrlidm  21375  psrridm  21376  psrass1  21377  psrdi  21378  psrdir  21379  mplsubglem  21408  mplvscaval  21423  subrgmvrf  21438  mplbas2  21446  mvrf2  21471  mplind  21481  psrbagev1  21488  psrbagev1OLD  21489  psrbagev2  21490  evlslem3  21493  evlslem1  21495  evlsvar  21503  mpfind  21520  ismhp3  21536  mhpmulcl  21542  psrplusgpropd  21610  coe1add  21638  coe1addfv  21639  evl1addd  21710  evl1subd  21711  evl1muld  21712  pf1mpf  21721  pf1ind  21724  mamudir  21754  mamulid  21793  mamurid  21794  mdetrlin  21954  mdetrsca  21955  mdetralt  21960  mdetunilem7  21970  mdetunilem9  21972  madurid  21996  cnrest2  22640  lmss  22652  lmcnp  22658  cnt0  22700  cnt1  22704  cnhaus  22708  rncmp  22750  conncn  22780  2ndcomap  22812  1stccnp  22816  comppfsc  22886  1stckgenlem  22907  ptbasfi  22935  ptopn  22937  ptclsg  22969  ptcnp  22976  upxp  22977  txtube  22994  txcmplem1  22995  hauseqlcld  23000  xkohaus  23007  xkoptsub  23008  cnmpt11  23017  cnmpt21  23025  cnmpt22f  23029  cnmptcom  23032  qtopss  23069  qtopeu  23070  qtopomap  23072  qtopcmap  23073  kqffn  23079  hmeof1o2  23117  xkocnv  23168  rnelfm  23307  ptcmplem1  23406  cnextfres1  23422  ghmcnp  23469  tgphaus  23471  prdstmdd  23478  prdstgpd  23479  fmucnd  23647  psmetxrge0  23669  isxmet2d  23683  prdsmet  23726  blelrnps  23772  blelrn  23773  xmetresbl  23793  comet  23872  stdbdxmet  23874  met2ndci  23881  prdsxmslem2  23888  isngp3  23957  nmotri  24106  metdsre  24219  bndth  24324  evth  24325  fmcfil  24639  bcthlem4  24694  rrxcph  24759  rrxds  24760  rrxmet  24775  evthicc2  24827  ovolfsf  24838  ovolmge0  24844  ovollb2lem  24855  ovolunlem1a  24863  ovoliunlem1  24869  ovoliun  24872  ovoliun2  24873  ovolscalem1  24880  ovolicc1  24883  ovolicc2lem4  24887  ovolicc2  24889  voliunlem1  24917  voliunlem3  24919  volsup  24923  ioombl1lem2  24926  ioombl1lem4  24928  uniiccdif  24945  uniioombllem2  24950  uniioombllem3  24952  uniioombllem6  24955  volsup2  24972  vitalilem4  24978  mbfeqalem1  25008  mbfmulc2lem  25014  mbfmax  25016  mbfaddlem  25027  mbfadd  25028  mbfsub  25029  mbfsup  25031  mbfinf  25032  itg1ge0  25053  itg1addlem1  25059  i1faddlem  25060  i1fmullem  25061  i1fadd  25062  i1fmul  25063  itg1addlem4  25066  itg1addlem4OLD  25067  i1fmulclem  25070  i1fmulc  25071  itg1mulc  25072  i1fres  25073  itg10a  25078  itg1ge0a  25079  itg1lea  25080  mbfi1fseqlem3  25085  mbfi1fseqlem4  25086  mbfi1flimlem  25090  mbfmullem2  25092  mbfmul  25094  itg20  25105  itg2lea  25112  itg2splitlem  25116  itg2split  25117  itg2monolem1  25118  itg2monolem2  25119  itg2monolem3  25120  itg2mono  25121  itg2i1fseqle  25122  itg2i1fseq  25123  itg2addlem  25126  itg2gt0  25128  itg2cnlem1  25129  itg2cnlem2  25130  itg2cn  25131  itgitg1  25176  bddmulibl  25206  bddibl  25207  dvidlem  25282  dvaddbr  25305  dvmulbr  25306  dvaddf  25309  dvcmulf  25312  dvrec  25322  dvcnvlem  25343  rolle  25357  dveq0  25367  dv11cn  25368  dvivthlem2  25376  dvivth  25377  dvne0  25378  lhop1lem  25380  lhop1  25381  lhop2  25382  lhop  25383  ftc1cn  25410  tdeglem1  25423  tdeglem3  25425  tdeglem4  25427  tdeglem4OLD  25428  mdegleb  25432  mdegldg  25434  mdegaddle  25442  ply1remlem  25530  ply1rem  25531  fta1glem1  25533  fta1glem2  25534  fta1blem  25536  plyeq0lem  25574  plyeq0  25575  plyaddlem1  25577  coeeulem  25588  coeaddlem  25613  coemulc  25619  dgradd2  25632  dgrcolem2  25638  ofmulrt  25645  plyrem  25668  vieta1lem1  25673  vieta1  25675  plyexmo  25676  elqaalem3  25684  aannenlem1  25691  aalioulem2  25696  ulmuni  25754  ulmdvlem1  25762  ulmdv  25765  mbfulm  25768  iblulm  25769  itgulm  25770  rlimcnp2  26319  jensen  26341  amgm  26343  basellem3  26435  basellem7  26439  basellem9  26441  dchrelbas2  26588  dchrmulcl  26600  dchrfi  26606  dchreq  26609  dchrresb  26610  dchrinv  26612  dchr1re  26614  sumdchr2  26621  dchr2sum  26624  lgsqrlem2  26698  lgsqrlem3  26699  rpvmasum2  26863  dchrisum0re  26864  mirf1o  27614  lmif1o  27740  eqeefv  27855  axlowdimlem14  27907  vtxdgfisf  28427  2pthon3v  28891  nvinvfval  29585  sspg  29673  ssps  29675  sspmlem  29677  sspn  29681  lnon0  29743  ubthlem1  29815  pjfn  30654  kbpj  30901  kbass2  31062  elpjrn  31135  ofrn2  31559  off2  31560  ofresid  31561  xppreima2  31570  ofpreima2  31585  suppovss  31601  resf1o  31650  swrdrn3  31812  pwrssmgc  31863  mgcf1o  31866  gsumhashmul  31901  gsumle  31935  symgcom2  31938  pmtrcnel  31943  pmtrcnel2  31944  pmtrcnelor  31945  cycpmfvlem  31964  cycpmfv3  31967  cycpmcl  31968  cycpmco2rn  31977  cycpmco2  31985  cycpm3cl2  31988  cyc3co2  31992  cyc3evpm  32002  islinds5  32159  ellspds  32160  ghmquskerlem1  32198  ghmquskerco  32199  ghmqusker  32201  rhmpreimaidl  32203  elrspunidl  32206  rhmimaidl  32209  rhmpreimaprmidl  32227  evls1fn  32270  evls1fpws  32274  ressply1evl  32275  dimkerim  32325  fedgmullem2  32328  fedgmul  32329  irngss  32364  irngnzply1  32368  cmpcref  32434  rhmpreimacnlem  32468  fsumcvg4  32534  pl1cn  32539  qqhval2lem  32565  prodindf  32625  indpreima  32627  esumcvg  32688  ofcf  32705  ofcof  32709  measfn  32806  meascnbl  32821  sibfof  32943  sitgaddlemb  32951  subiwrdlen  32989  rrvfn  33048  plymul02  33161  signsplypnf  33165  signsply0  33166  reprsuc  33231  reprdifc  33243  breprexplema  33246  circlemethhgt  33259  hgt750lemb  33272  f1resrcmplf1dlem  33693  pthhashvtx  33724  cvmopnlem  33875  cvmliftmolem1  33878  cvmliftlem10  33891  cvmlift2lem9a  33900  cvmlift2lem6  33905  cvmlift2lem12  33911  cvmliftphtlem  33914  cvmlift3lem9  33924  mrsubrn  34110  elmrsubrn  34117  elmsubrn  34125  msubrn  34126  mclsind  34167  mclsppslem  34180  mclspps  34181  iprodefisumlem  34316  matunitlindflem1  36077  poimirlem1  36082  poimirlem2  36083  poimirlem3  36084  poimirlem16  36097  poimirlem17  36098  poimirlem19  36100  poimirlem20  36101  poimirlem22  36103  poimirlem23  36104  poimirlem29  36110  poimirlem30  36111  poimirlem31  36112  poimir  36114  mblfinlem2  36119  itg2addnclem3  36134  itg2addnc  36135  itg2gt0cn  36136  ftc1cnnc  36153  ftc1anclem5  36158  ftc1anclem7  36160  ftc1anc  36162  sdclem2  36204  istotbnd3  36233  sstotbnd2  36236  isbnd3  36246  heibor1lem  36271  rrnmet  36291  grpokerinj  36355  isdrngo2  36420  lfl1  37535  lfladdcl  37536  lflvscl  37542  lkr0f  37559  lkrsc  37562  eqlkr2  37565  eqlkr3  37566  ldualvaddval  37596  ldualvsval  37603  tendoeq1  39230  sticksstones1  40557  sticksstones2  40558  sticksstones3  40559  sticksstones12a  40568  sticksstones12  40569  metakunt19  40598  metakunt25  40604  metakunt33  40612  frlmvscadiccat  40684  imadrhmcl  40719  frlmsnic  40731  pwsgprod  40735  evlsbagval  40751  evlsaddval  40753  evlsmulval  40754  evladdval  40756  evlmulval  40757  fsuppssind  40771  mhphf  40774  ismrcd1  41024  ismrcd2  41025  istopclsd  41026  isnacs3  41036  mzpaddmpt  41067  mzpmulmpt  41068  mzpsubst  41074  mzpcong  41299  fnwe2lem2  41381  islmodfg  41399  kercvrlsm  41413  dgrsub2  41465  mpaaeu  41480  rngunsnply  41503  idomrootle  41525  hausgraph  41542  ofoafg  41671  ofoafo  41673  ofoaid1  41675  ofoaid2  41676  naddcnff  41679  naddcnffn  41680  naddcnffo  41681  naddcnfcom  41683  naddcnfid1  41684  naddcnfass  41686  fsovf1od  42295  brcoffn  42309  clsneiel1  42387  wfximgfd  42443  extoimad  42444  mnringmulrcld  42515  mnurndlem1  42568  caofcan  42610  ofmul12  42612  ofdivrec  42613  ofdivcan4  42614  ofdivdiv2  42615  dvconstbi  42621  binomcxplemnotnn0  42643  refsum2cnlem1  43249  ssmapsn  43444  preimaiocmnf  43806  fsumsupp0  43826  fsumsermpt  43827  climinf  43854  climinf2lem  43954  limsupmnflem  43968  limsupvaluz2  43986  supcnvlimsup  43988  limsupgtlem  44025  liminfvalxr  44031  liminflelimsupuz  44033  xlimconst2  44083  climxlim2  44094  icccncfext  44135  dvnprodlem1  44194  volicoff  44243  voliooicof  44244  fourierdlem25  44380  etransclem2  44484  etransclem35  44517  fge0iccico  44618  sge0tsms  44628  sge0sup  44639  sge0resrn  44652  sge0le  44655  sge0fodjrnlem  44664  sge0isum  44675  sge0seq  44694  nnfoctbdjlem  44703  meadjiunlem  44713  omeiunle  44765  hoicvr  44796  ovolval4lem1  44897  ovolval5lem3  44902  ovnovollem1  44904  ovnovollem2  44905  iinhoiicclem  44921  iunhoiioolem  44923  preimaicomnf  44959  smfresal  45036  smfsuplem1  45059  smflimsuplem2  45069  fcoreslem3  45306  fcoreslem4  45307  fcores  45308  mgmhmf1o  46088  resmgmhm2b  46101  mgmhmima  46103  mgmhmeql  46104  rnghmf1o  46208  ackvalsucsucval  46781  amgmwlem  47256
  Copyright terms: Public domain W3C validator