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

Theorem fdmd 6680
Description: Deduction form of fdm 6678. The domain of a mapping. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
Hypothesis
Ref Expression
fdmd.1 (𝜑𝐹:𝐴𝐵)
Assertion
Ref Expression
fdmd (𝜑 → dom 𝐹 = 𝐴)

Proof of Theorem fdmd
StepHypRef Expression
1 fdmd.1 . 2 (𝜑𝐹:𝐴𝐵)
2 fdm 6678 . 2 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
31, 2syl 17 1 (𝜑 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  dom cdm 5634  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-fn 6500  df-f 6501
This theorem is referenced by:  fssdmd  6688  fssdm  6689  foima  6762  focnvimacdmdm  6769  resdif  6806  fmptco  7076  funfvima2d  7183  focdmex  7889  suppsnop  8110  onnseq  8291  fopwdom  9025  fodomfib  9271  intrnfi  9353  ordtypelem5  9459  ordtypelem6  9460  ordtypelem7  9461  ordtypelem8  9462  brwdomn0  9506  wdomtr  9512  fseqenlem2  9962  fin23lem30  10279  isf34lem5  10315  isf34lem7  10316  isf34lem6  10317  fin1a2lem7  10343  ttukeylem6  10451  fodomb  10463  pwxpndom2  10602  hashf1lem1  14354  hashf1lem1OLD  14355  wrddm  14410  swrdcl  14534  cats1un  14610  repswswrd  14673  limsupgle  15360  limsupgre  15364  rlim  15378  rlimi  15396  lo1o1  15415  rlimuni  15433  o1co  15469  rlimcn1  15471  ruclem11  16123  1arith  16800  ramval  16881  0ram  16893  mrcuni  17502  homarcl2  17922  prfval  18088  gsumval  18533  gsumval2  18542  frmdss2  18674  ghmrn  19022  cntzmhm2  19121  gsumval3  19685  gsumzaddlem  19699  dmdprdd  19779  dprdres  19808  dprdf1  19813  dprd2da  19822  dmdprdsplit2lem  19825  dmdprdsplit2  19826  dmdprdsplit  19827  dprdsplit  19828  dpjidcl  19838  ablfac1eulem  19852  ablfac1eu  19853  ablfaclem2  19866  ablfac2  19869  lmhmlsp  20513  frlmsslsp  21205  f1lindf  21231  mattpostpos  21806  iinopn  22254  lmbrf  22614  cnntri  22625  cnclsi  22626  lmcnp  22658  cnt0  22700  cnt1  22704  cnhaus  22708  cncmp  22746  connima  22779  1stcfb  22799  1stccnp  22816  1stckgenlem  22907  kgencn3  22912  txcnpi  22962  txcnp  22974  prdstps  22983  xkohaus  23007  xkoco2cn  23012  qtopeu  23070  hmeores  23125  fmfnfmlem2  23309  fmfnfmlem4  23311  fmfnfm  23312  lmflf  23359  txflf  23360  cnextfval  23416  cnextcn  23421  clssubg  23463  ghmcnp  23469  qustgplem  23475  tsmsval  23485  ucncn  23640  xmetdmdm  23691  metn0  23716  tmsval  23839  metustid  23913  metustexhalf  23915  metustfbas  23916  isngp2  23956  evth  24325  lmmbrf  24629  iscfil2  24633  caufval  24642  iscau2  24644  caucfil  24650  ovollb2  24856  ovolunlem1a  24863  ovoliunlem1  24869  ovoliun2  24873  ioombl1lem4  24928  uniioombllem1  24948  uniioombllem2  24950  uniioombllem6  24955  mbfconstlem  24994  ismbfcn  24996  mbfmulc2lem  25014  mbfmulc2re  25015  cncombf  25025  mbfaddlem  25027  mbflimsup  25033  i1f0rn  25049  itg1addlem5  25068  itg1climres  25082  mbfmullem2  25092  limcfval  25239  limcdif  25243  ellimc2  25244  ellimc3  25246  limccnp  25258  dvfval  25264  cpnord  25302  cpnres  25304  dvcmul  25311  dvcmulf  25312  dvexp  25320  dvgt0lem1  25369  dvcnvrelem1  25384  itgpowd  25417  plyaddlem1  25577  plymullem1  25578  plycpn  25652  aalioulem3  25697  tayl0  25724  dvntaylp  25733  ulm2  25747  ulmdvlem1  25762  xrlimcnp  26321  dchrelbas2  26588  dchrghm  26607  dchrptlem1  26615  dchrptlem2  26616  iscgrgd  27458  iscgrglt  27459  trgcgrg  27460  tgcgr4  27476  motcgrg  27489  wrdupgr  28039  wrdumgr  28051  grporndm  29455  sspn  29681  fmptcof2  31576  fnpreimac  31590  curry2ima  31625  fpwrelmap  31653  swrdf1  31813  pmtrcnel  31943  pmtrcnel2  31944  pmtrcnelor  31945  cycpmcl  31968  cycpmco2f1  31976  cycpmco2rn  31977  cycpmco2lem1  31978  cycpmco2lem2  31979  cycpmco2lem3  31980  cycpmco2lem4  31981  cycpmco2lem5  31982  cycpmco2lem6  31983  cycpmco2lem7  31984  cycpmco2  31985  cyc3co2  31992  cycpmconjv  31994  rmfsupp2  32078  rhmpreimaidl  32203  elrspunidl  32206  rhmimaidl  32209  irngnzply1lem  32367  irngnzply1  32368  zarcmplem  32465  rhmpreimacnlem  32468  indf1ofs  32628  esumpcvgval  32680  ofcfval4  32707  measdivcst  32826  oms0  32900  omsmon  32901  omssubaddlem  32902  omssubadd  32903  carsgval  32906  omsmeas  32926  sitgclg  32945  eulerpartlemgu  32980  sseqfv2  32997  rrvdm  33049  ftc2re  33214  cvmliftmolem1  33878  cvmliftlem3  33884  cvmliftlem10  33891  cvmliftlem13  33893  cvmlift2lem9  33908  cvmlift3lem6  33921  cvmlift3lem7  33922  mclsax  34166  mclsppslem  34180  mclspps  34181  fwddifval  34750  fwddifnval  34751  bj-finsumval0  35759  curunc  36063  itg2addnclem2  36133  ftc1anclem5  36158  ftc1anclem6  36159  ftc1anclem8  36161  sdclem2  36204  isbnd3  36246  ssbnd  36250  bnd2lem  36253  ismtyval  36262  grpokerinj  36355  rngosn3  36386  rngodm1dm2  36394  divrngcl  36419  isdrngo2  36420  sticksstones1  40557  mapfzcons2  41045  fnwe2lem2  41381  lmhmfgima  41414  wnefimgd  42441  binomcxplemnotnn0  42643  cncmpmax  43244  mullimcf  43871  limsuppnfdlem  43949  limsupvaluz  43956  climxrrelem  43997  climxrre  43998  liminfvalxr  44031  liminflimsupxrre  44065  xlimmnfvlem2  44081  xlimpnfvlem2  44085  xlimliminflimsup  44110  cncfuni  44134  cncficcgt0  44136  cncfioobd  44145  dvsinax  44161  itgperiod  44229  fvvolioof  44237  fvvolicof  44239  stoweidlem29  44277  fourierdlem20  44375  fourierdlem53  44407  fourierdlem63  44417  fourierdlem68  44422  fourierdlem82  44436  sge0sn  44627  sge0tsms  44628  sge0cl  44629  sge0isum  44675  ismeannd  44715  hoicvr  44796  dmovn  44852  hspmbl  44877  ovolval4lem1  44897  ovnovollem1  44904  ovnovollem2  44905  issmfd  44983  issmfdf  44985  cnfsmf  44988  issmfled  45005  issmfgtd  45009  smfsuplem1  45059  smfdivdmmbl2  45089  fcores  45308  f1cof1blem  45315  f1cof1b  45316  funfocofob  45317  rmsuppss  46453  mndpsuppss  46454  itcovalendof  46762
  Copyright terms: Public domain W3C validator