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

Theorem fdmd 6496
Description: Deduction form of fdm 6495. 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 6495 . 2 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
31, 2syl 17 1 (𝜑 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  dom cdm 5528  wf 6324
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 210  df-an 400  df-fn 6331  df-f 6332
This theorem is referenced by:  fssdmd  6502  fssdm  6503  foima  6568  resdif  6608  fmptco  6864  funfvima2d  6968  fornex  7632  suppsnop  7819  onnseq  7956  fopwdom  8600  fodomfib  8774  intrnfi  8856  ordtypelem5  8962  ordtypelem6  8963  ordtypelem7  8964  ordtypelem8  8965  brwdomn0  9009  wdomtr  9015  fseqenlem2  9428  fin23lem30  9741  isf34lem5  9777  isf34lem7  9778  isf34lem6  9779  fin1a2lem7  9805  ttukeylem6  9913  fodomb  9925  pwxpndom2  10064  hashf1lem1  13797  wrddm  13852  swrdcl  13986  cats1un  14062  repswswrd  14125  limsupgle  14813  limsupgre  14817  rlim  14831  rlimi  14849  lo1o1  14868  rlimuni  14886  o1co  14922  rlimcn1  14924  ruclem11  15572  1arith  16240  ramval  16321  0ram  16333  mrcuni  16870  homarcl2  17273  prfval  17427  gsumval  17865  gsumval2  17874  frmdss2  18006  ghmrn  18349  cntzmhm2  18448  gsumval3  19005  gsumzaddlem  19019  dmdprdd  19099  dprdres  19128  dprdf1  19133  dprd2da  19142  dmdprdsplit2lem  19145  dmdprdsplit2  19146  dmdprdsplit  19147  dprdsplit  19148  dpjidcl  19158  ablfac1eulem  19172  ablfac1eu  19173  ablfaclem2  19186  ablfac2  19189  lmhmlsp  19796  frlmsslsp  20915  f1lindf  20941  mattpostpos  21038  iinopn  21485  lmbrf  21843  cnntri  21854  cnclsi  21855  lmcnp  21887  cnt0  21929  cnt1  21933  cnhaus  21937  cncmp  21975  connima  22008  1stcfb  22028  1stccnp  22045  1stckgenlem  22136  kgencn3  22141  txcnpi  22191  txcnp  22203  prdstps  22212  xkohaus  22236  xkoco2cn  22241  qtopeu  22299  hmeores  22354  fmfnfmlem2  22538  fmfnfmlem4  22540  fmfnfm  22541  lmflf  22588  txflf  22589  cnextfval  22645  cnextcn  22650  clssubg  22692  ghmcnp  22698  qustgplem  22704  tsmsval  22714  ucncn  22869  xmetdmdm  22920  metn0  22945  tmsval  23066  metustid  23139  metustexhalf  23141  metustfbas  23142  isngp2  23181  evth  23542  lmmbrf  23844  iscfil2  23848  caufval  23857  iscau2  23859  caucfil  23865  ovollb2  24071  ovolunlem1a  24078  ovoliunlem1  24084  ovoliun2  24088  ioombl1lem4  24143  uniioombllem1  24163  uniioombllem2  24165  uniioombllem6  24170  mbfconstlem  24209  ismbfcn  24211  mbfmulc2lem  24229  mbfmulc2re  24230  cncombf  24240  mbfaddlem  24242  mbflimsup  24248  i1f0rn  24264  itg1addlem5  24282  itg1climres  24296  mbfmullem2  24306  limcfval  24453  limcdif  24457  ellimc2  24458  ellimc3  24460  limccnp  24472  dvfval  24478  cpnord  24516  cpnres  24518  dvcmul  24525  dvcmulf  24526  dvexp  24534  dvgt0lem1  24583  dvcnvrelem1  24598  itgpowd  24631  plyaddlem1  24788  plymullem1  24789  plycpn  24863  aalioulem3  24908  tayl0  24935  dvntaylp  24944  ulm2  24958  ulmdvlem1  24973  xrlimcnp  25532  dchrelbas2  25799  dchrghm  25818  dchrptlem1  25826  dchrptlem2  25827  iscgrgd  26285  iscgrglt  26286  trgcgrg  26287  tgcgr4  26303  motcgrg  26316  wrdupgr  26856  wrdumgr  26868  grporndm  28271  sspn  28497  fmptcof2  30388  fnpreimac  30402  curry2ima  30430  fpwrelmap  30455  swrdf1  30616  pmtrcnel  30740  pmtrcnel2  30741  pmtrcnelor  30742  cycpmcl  30765  cycpmco2f1  30773  cycpmco2rn  30774  cycpmco2lem1  30775  cycpmco2lem2  30776  cycpmco2lem3  30777  cycpmco2lem4  30778  cycpmco2lem5  30779  cycpmco2lem6  30780  cycpmco2lem7  30781  cycpmco2  30782  cyc3co2  30789  cycpmconjv  30791  rmfsupp2  30873  indf1ofs  31292  esumpcvgval  31344  ofcfval4  31371  measdivcst  31490  oms0  31562  omsmon  31563  omssubaddlem  31564  omssubadd  31565  carsgval  31568  omsmeas  31588  sitgclg  31607  eulerpartlemgu  31642  sseqfv2  31659  rrvdm  31711  ftc2re  31876  cvmliftmolem1  32535  cvmliftlem3  32541  cvmliftlem10  32548  cvmliftlem13  32550  cvmlift2lem9  32565  cvmlift3lem6  32578  cvmlift3lem7  32579  mclsax  32823  mclsppslem  32837  mclspps  32838  fwddifval  33630  fwddifnval  33631  bj-finsumval0  34583  curunc  34919  itg2addnclem2  34989  ftc1anclem5  35014  ftc1anclem6  35015  ftc1anclem8  35017  sdclem2  35060  isbnd3  35102  ssbnd  35106  bnd2lem  35109  ismtyval  35118  grpokerinj  35211  rngosn3  35242  rngodm1dm2  35250  divrngcl  35275  isdrngo2  35276  mapfzcons2  39457  fnwe2lem2  39792  lmhmfgima  39825  wnefimgd  40649  binomcxplemnotnn0  40845  cncmpmax  41446  mullimcf  42058  limsuppnfdlem  42136  limsupvaluz  42143  climxrrelem  42184  climxrre  42185  liminfvalxr  42218  liminflimsupxrre  42252  xlimmnfvlem2  42268  xlimpnfvlem2  42272  xlimliminflimsup  42297  cncfuni  42321  cncficcgt0  42323  cncfioobd  42332  dvsinax  42348  itgperiod  42416  fvvolioof  42424  fvvolicof  42426  stoweidlem29  42464  fourierdlem20  42562  fourierdlem53  42594  fourierdlem63  42604  fourierdlem68  42609  fourierdlem82  42623  sge0sn  42811  sge0tsms  42812  sge0cl  42813  sge0isum  42859  ismeannd  42899  hoicvr  42980  dmovn  43036  hspmbl  43061  ovolval4lem1  43081  ovnovollem1  43088  ovnovollem2  43089  issmfd  43162  issmfdf  43164  cnfsmf  43167  issmfled  43184  issmfgtd  43187  smfsuplem1  43235  rmsuppss  44565  mndpsuppss  44566  itcovalendof  44845
  Copyright terms: Public domain W3C validator