Theorem fdmd 6497

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

Step	Hyp	Ref	Expression
1		fdmd.1	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		fdm 6495	. 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1538  dom cdm 5519  ⟶wf 6320

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 6327  df-f 6328

This theorem is referenced by:  fssdmd  6503  fssdm  6504  foima  6570  resdif  6610  fmptco  6868  funfvima2d  6972  fornex  7639  suppsnop  7827  onnseq  7964  fopwdom  8608  fodomfib  8782  intrnfi  8864  ordtypelem5  8970  ordtypelem6  8971  ordtypelem7  8972  ordtypelem8  8973  brwdomn0  9017  wdomtr  9023  fseqenlem2  9436  fin23lem30  9753  isf34lem5  9789  isf34lem7  9790  isf34lem6  9791  fin1a2lem7  9817  ttukeylem6  9925  fodomb  9937  pwxpndom2  10076  hashf1lem1  13809  wrddm  13864  swrdcl  13998  cats1un  14074  repswswrd  14137  limsupgle  14826  limsupgre  14830  rlim  14844  rlimi  14862  lo1o1  14881  rlimuni  14899  o1co  14935  rlimcn1  14937  ruclem11  15585  1arith  16253  ramval  16334  0ram  16346  mrcuni  16884  homarcl2  17287  prfval  17441  gsumval  17879  gsumval2  17888  frmdss2  18020  ghmrn  18363  cntzmhm2  18462  gsumval3  19020  gsumzaddlem  19034  dmdprdd  19114  dprdres  19143  dprdf1  19148  dprd2da  19157  dmdprdsplit2lem  19160  dmdprdsplit2  19161  dmdprdsplit  19162  dprdsplit  19163  dpjidcl  19173  ablfac1eulem  19187  ablfac1eu  19188  ablfaclem2  19201  ablfac2  19204  lmhmlsp  19814  frlmsslsp  20485  f1lindf  20511  mattpostpos  21059  iinopn  21507  lmbrf  21865  cnntri  21876  cnclsi  21877  lmcnp  21909  cnt0  21951  cnt1  21955  cnhaus  21959  cncmp  21997  connima  22030  1stcfb  22050  1stccnp  22067  1stckgenlem  22158  kgencn3  22163  txcnpi  22213  txcnp  22225  prdstps  22234  xkohaus  22258  xkoco2cn  22263  qtopeu  22321  hmeores  22376  fmfnfmlem2  22560  fmfnfmlem4  22562  fmfnfm  22563  lmflf  22610  txflf  22611  cnextfval  22667  cnextcn  22672  clssubg  22714  ghmcnp  22720  qustgplem  22726  tsmsval  22736  ucncn  22891  xmetdmdm  22942  metn0  22967  tmsval  23088  metustid  23161  metustexhalf  23163  metustfbas  23164  isngp2  23203  evth  23564  lmmbrf  23866  iscfil2  23870  caufval  23879  iscau2  23881  caucfil  23887  ovollb2  24093  ovolunlem1a  24100  ovoliunlem1  24106  ovoliun2  24110  ioombl1lem4  24165  uniioombllem1  24185  uniioombllem2  24187  uniioombllem6  24192  mbfconstlem  24231  ismbfcn  24233  mbfmulc2lem  24251  mbfmulc2re  24252  cncombf  24262  mbfaddlem  24264  mbflimsup  24270  i1f0rn  24286  itg1addlem5  24304  itg1climres  24318  mbfmullem2  24328  limcfval  24475  limcdif  24479  ellimc2  24480  ellimc3  24482  limccnp  24494  dvfval  24500  cpnord  24538  cpnres  24540  dvcmul  24547  dvcmulf  24548  dvexp  24556  dvgt0lem1  24605  dvcnvrelem1  24620  itgpowd  24653  plyaddlem1  24810  plymullem1  24811  plycpn  24885  aalioulem3  24930  tayl0  24957  dvntaylp  24966  ulm2  24980  ulmdvlem1  24995  xrlimcnp  25554  dchrelbas2  25821  dchrghm  25840  dchrptlem1  25848  dchrptlem2  25849  iscgrgd  26307  iscgrglt  26308  trgcgrg  26309  tgcgr4  26325  motcgrg  26338  wrdupgr  26878  wrdumgr  26890  grporndm  28293  sspn  28519  fmptcof2  30420  fnpreimac  30434  curry2ima  30468  fpwrelmap  30495  swrdf1  30656  pmtrcnel  30783  pmtrcnel2  30784  pmtrcnelor  30785  cycpmcl  30808  cycpmco2f1  30816  cycpmco2rn  30817  cycpmco2lem1  30818  cycpmco2lem2  30819  cycpmco2lem3  30820  cycpmco2lem4  30821  cycpmco2lem5  30822  cycpmco2lem6  30823  cycpmco2lem7  30824  cycpmco2  30825  cyc3co2  30832  cycpmconjv  30834  rmfsupp2  30917  rhmpreimaidl  31011  elrspunidl  31014  rhmimaidl  31017  zarcmplem  31234  rhmpreimacnlem  31237  indf1ofs  31395  esumpcvgval  31447  ofcfval4  31474  measdivcst  31593  oms0  31665  omsmon  31666  omssubaddlem  31667  omssubadd  31668  carsgval  31671  omsmeas  31691  sitgclg  31710  eulerpartlemgu  31745  sseqfv2  31762  rrvdm  31814  ftc2re  31979  cvmliftmolem1  32641  cvmliftlem3  32647  cvmliftlem10  32654  cvmliftlem13  32656  cvmlift2lem9  32671  cvmlift3lem6  32684  cvmlift3lem7  32685  mclsax  32929  mclsppslem  32943  mclspps  32944  fwddifval  33736  fwddifnval  33737  bj-finsumval0  34700  curunc  35039  itg2addnclem2  35109  ftc1anclem5  35134  ftc1anclem6  35135  ftc1anclem8  35137  sdclem2  35180  isbnd3  35222  ssbnd  35226  bnd2lem  35229  ismtyval  35238  grpokerinj  35331  rngosn3  35362  rngodm1dm2  35370  divrngcl  35395  isdrngo2  35396  mapfzcons2  39660  fnwe2lem2  39995  lmhmfgima  40028  wnefimgd  40865  binomcxplemnotnn0  41060  cncmpmax  41661  mullimcf  42265  limsuppnfdlem  42343  limsupvaluz  42350  climxrrelem  42391  climxrre  42392  liminfvalxr  42425  liminflimsupxrre  42459  xlimmnfvlem2  42475  xlimpnfvlem2  42479  xlimliminflimsup  42504  cncfuni  42528  cncficcgt0  42530  cncfioobd  42539  dvsinax  42555  itgperiod  42623  fvvolioof  42631  fvvolicof  42633  stoweidlem29  42671  fourierdlem20  42769  fourierdlem53  42801  fourierdlem63  42811  fourierdlem68  42816  fourierdlem82  42830  sge0sn  43018  sge0tsms  43019  sge0cl  43020  sge0isum  43066  ismeannd  43106  hoicvr  43187  dmovn  43243  hspmbl  43268  ovolval4lem1  43288  ovnovollem1  43295  ovnovollem2  43296  issmfd  43369  issmfdf  43371  cnfsmf  43374  issmfled  43391  issmfgtd  43394  smfsuplem1  43442  rmsuppss  44772  mndpsuppss  44773  itcovalendof  45083