Theorem fdmd 6595

Description: Deduction form of fdm 6593. 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 6593	. 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1539  dom cdm 5580  ⟶wf 6414

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 396  df-fn 6421  df-f 6422

This theorem is referenced by:  fssdmd  6603  fssdm  6604  foima  6677  focnvimacdmdm  6684  resdif  6720  fmptco  6983  funfvima2d  7090  fornex  7772  suppsnop  7965  onnseq  8146  fopwdom  8820  fodomfib  9023  intrnfi  9105  ordtypelem5  9211  ordtypelem6  9212  ordtypelem7  9213  ordtypelem8  9214  brwdomn0  9258  wdomtr  9264  fseqenlem2  9712  fin23lem30  10029  isf34lem5  10065  isf34lem7  10066  isf34lem6  10067  fin1a2lem7  10093  ttukeylem6  10201  fodomb  10213  pwxpndom2  10352  hashf1lem1  14096  hashf1lem1OLD  14097  wrddm  14152  swrdcl  14286  cats1un  14362  repswswrd  14425  limsupgle  15114  limsupgre  15118  rlim  15132  rlimi  15150  lo1o1  15169  rlimuni  15187  o1co  15223  rlimcn1  15225  ruclem11  15877  1arith  16556  ramval  16637  0ram  16649  mrcuni  17247  homarcl2  17666  prfval  17832  gsumval  18276  gsumval2  18285  frmdss2  18417  ghmrn  18762  cntzmhm2  18861  gsumval3  19423  gsumzaddlem  19437  dmdprdd  19517  dprdres  19546  dprdf1  19551  dprd2da  19560  dmdprdsplit2lem  19563  dmdprdsplit2  19564  dmdprdsplit  19565  dprdsplit  19566  dpjidcl  19576  ablfac1eulem  19590  ablfac1eu  19591  ablfaclem2  19604  ablfac2  19607  lmhmlsp  20226  frlmsslsp  20913  f1lindf  20939  mattpostpos  21511  iinopn  21959  lmbrf  22319  cnntri  22330  cnclsi  22331  lmcnp  22363  cnt0  22405  cnt1  22409  cnhaus  22413  cncmp  22451  connima  22484  1stcfb  22504  1stccnp  22521  1stckgenlem  22612  kgencn3  22617  txcnpi  22667  txcnp  22679  prdstps  22688  xkohaus  22712  xkoco2cn  22717  qtopeu  22775  hmeores  22830  fmfnfmlem2  23014  fmfnfmlem4  23016  fmfnfm  23017  lmflf  23064  txflf  23065  cnextfval  23121  cnextcn  23126  clssubg  23168  ghmcnp  23174  qustgplem  23180  tsmsval  23190  ucncn  23345  xmetdmdm  23396  metn0  23421  tmsval  23542  metustid  23616  metustexhalf  23618  metustfbas  23619  isngp2  23659  evth  24028  lmmbrf  24331  iscfil2  24335  caufval  24344  iscau2  24346  caucfil  24352  ovollb2  24558  ovolunlem1a  24565  ovoliunlem1  24571  ovoliun2  24575  ioombl1lem4  24630  uniioombllem1  24650  uniioombllem2  24652  uniioombllem6  24657  mbfconstlem  24696  ismbfcn  24698  mbfmulc2lem  24716  mbfmulc2re  24717  cncombf  24727  mbfaddlem  24729  mbflimsup  24735  i1f0rn  24751  itg1addlem5  24770  itg1climres  24784  mbfmullem2  24794  limcfval  24941  limcdif  24945  ellimc2  24946  ellimc3  24948  limccnp  24960  dvfval  24966  cpnord  25004  cpnres  25006  dvcmul  25013  dvcmulf  25014  dvexp  25022  dvgt0lem1  25071  dvcnvrelem1  25086  itgpowd  25119  plyaddlem1  25279  plymullem1  25280  plycpn  25354  aalioulem3  25399  tayl0  25426  dvntaylp  25435  ulm2  25449  ulmdvlem1  25464  xrlimcnp  26023  dchrelbas2  26290  dchrghm  26309  dchrptlem1  26317  dchrptlem2  26318  iscgrgd  26778  iscgrglt  26779  trgcgrg  26780  tgcgr4  26796  motcgrg  26809  wrdupgr  27358  wrdumgr  27370  grporndm  28773  sspn  28999  fmptcof2  30896  fnpreimac  30910  curry2ima  30943  fpwrelmap  30970  swrdf1  31130  pmtrcnel  31260  pmtrcnel2  31261  pmtrcnelor  31262  cycpmcl  31285  cycpmco2f1  31293  cycpmco2rn  31294  cycpmco2lem1  31295  cycpmco2lem2  31296  cycpmco2lem3  31297  cycpmco2lem4  31298  cycpmco2lem5  31299  cycpmco2lem6  31300  cycpmco2lem7  31301  cycpmco2  31302  cyc3co2  31309  cycpmconjv  31311  rmfsupp2  31394  rhmpreimaidl  31505  elrspunidl  31508  rhmimaidl  31511  zarcmplem  31733  rhmpreimacnlem  31736  indf1ofs  31894  esumpcvgval  31946  ofcfval4  31973  measdivcst  32092  oms0  32164  omsmon  32165  omssubaddlem  32166  omssubadd  32167  carsgval  32170  omsmeas  32190  sitgclg  32209  eulerpartlemgu  32244  sseqfv2  32261  rrvdm  32313  ftc2re  32478  cvmliftmolem1  33143  cvmliftlem3  33149  cvmliftlem10  33156  cvmliftlem13  33158  cvmlift2lem9  33173  cvmlift3lem6  33186  cvmlift3lem7  33187  mclsax  33431  mclsppslem  33445  mclspps  33446  fwddifval  34391  fwddifnval  34392  bj-finsumval0  35383  curunc  35686  itg2addnclem2  35756  ftc1anclem5  35781  ftc1anclem6  35782  ftc1anclem8  35784  sdclem2  35827  isbnd3  35869  ssbnd  35873  bnd2lem  35876  ismtyval  35885  grpokerinj  35978  rngosn3  36009  rngodm1dm2  36017  divrngcl  36042  isdrngo2  36043  sticksstones1  40030  mapfzcons2  40457  fnwe2lem2  40792  lmhmfgima  40825  wnefimgd  41661  binomcxplemnotnn0  41863  cncmpmax  42464  mullimcf  43054  limsuppnfdlem  43132  limsupvaluz  43139  climxrrelem  43180  climxrre  43181  liminfvalxr  43214  liminflimsupxrre  43248  xlimmnfvlem2  43264  xlimpnfvlem2  43268  xlimliminflimsup  43293  cncfuni  43317  cncficcgt0  43319  cncfioobd  43328  dvsinax  43344  itgperiod  43412  fvvolioof  43420  fvvolicof  43422  stoweidlem29  43460  fourierdlem20  43558  fourierdlem53  43590  fourierdlem63  43600  fourierdlem68  43605  fourierdlem82  43619  sge0sn  43807  sge0tsms  43808  sge0cl  43809  sge0isum  43855  ismeannd  43895  hoicvr  43976  dmovn  44032  hspmbl  44057  ovolval4lem1  44077  ovnovollem1  44084  ovnovollem2  44085  issmfd  44158  issmfdf  44160  cnfsmf  44163  issmfled  44180  issmfgtd  44183  smfsuplem1  44231  fcores  44448  f1cof1blem  44455  f1cof1b  44456  funfocofob  44457  rmsuppss  45594  mndpsuppss  45595  itcovalendof  45903