Theorem fdmd 6672

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

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5624  ⟶wf 6488

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 207  df-an 396  df-fn 6495  df-f 6496

This theorem is referenced by:  fssdmd  6680  fssdm  6681  foima  6751  focnvimacdmdm  6758  resdif  6795  fssrescdmd  7071  fmptco  7074  funfvima2d  7178  focdmex  7900  suppsnop  8120  onnseq  8276  fopwdom  9013  fodomfib  9229  fodomfibOLD  9231  intrnfi  9319  ordtypelem5  9427  ordtypelem6  9428  ordtypelem7  9429  ordtypelem8  9430  brwdomn0  9474  wdomtr  9480  fseqenlem2  9935  fin23lem30  10252  isf34lem5  10288  isf34lem7  10289  isf34lem6  10290  fin1a2lem7  10316  ttukeylem6  10424  fodomb  10436  pwxpndom2  10576  hashf1lem1  14378  wrddm  14444  ccatdmss  14505  swrdcl  14569  cats1un  14644  repswswrd  14707  limsupgle  15400  limsupgre  15404  rlim  15418  rlimi  15436  lo1o1  15455  rlimuni  15473  o1co  15509  rlimcn1  15511  ruclem11  16165  1arith  16855  ramval  16936  0ram  16948  mrcuni  17544  homarcl2  17959  prfval  18122  pfxchn  18533  chnind  18544  chnccats1  18548  chnccat  18549  gsumval  18602  gsumval2  18611  mndpsuppss  18690  frmdss2  18788  ghmrn  19158  cntzmhm2  19271  gsumval3  19836  gsumzaddlem  19850  dmdprdd  19930  dprdres  19959  dprdf1  19964  dprd2da  19973  dmdprdsplit2lem  19976  dmdprdsplit2  19977  dmdprdsplit  19978  dprdsplit  19979  dpjidcl  19989  ablfac1eulem  20003  ablfac1eu  20004  ablfaclem2  20017  ablfac2  20020  lmhmlsp  21001  rhmpreimaidl  21232  frlmsslsp  21751  f1lindf  21777  mattpostpos  22398  iinopn  22846  lmbrf  23204  cnntri  23215  cnclsi  23216  lmcnp  23248  cnt0  23290  cnt1  23294  cnhaus  23298  cncmp  23336  connima  23369  1stcfb  23389  1stccnp  23406  1stckgenlem  23497  kgencn3  23502  txcnpi  23552  txcnp  23564  prdstps  23573  xkohaus  23597  xkoco2cn  23602  qtopeu  23660  hmeores  23715  fmfnfmlem2  23899  fmfnfmlem4  23901  fmfnfm  23902  lmflf  23949  txflf  23950  cnextfval  24006  cnextcn  24011  clssubg  24053  ghmcnp  24059  qustgplem  24065  tsmsval  24075  ucncn  24228  xmetdmdm  24279  metn0  24304  tmsval  24425  metustid  24498  metustexhalf  24500  metustfbas  24501  isngp2  24541  evth  24914  lmmbrf  25218  iscfil2  25222  caufval  25231  iscau2  25233  caucfil  25239  ovollb2  25446  ovolunlem1a  25453  ovoliunlem1  25459  ovoliun2  25463  ioombl1lem4  25518  uniioombllem1  25538  uniioombllem2  25540  uniioombllem6  25545  mbfconstlem  25584  ismbfcn  25586  mbfmulc2lem  25604  mbfmulc2re  25605  cncombf  25615  mbfaddlem  25617  mbflimsup  25623  i1f0rn  25639  itg1addlem5  25657  itg1climres  25671  mbfmullem2  25681  limcfval  25829  limcdif  25833  ellimc2  25834  ellimc3  25836  limccnp  25848  dvfval  25854  cpnord  25893  cpnres  25895  dvcmul  25903  dvcmulf  25904  dvexp  25913  dvgt0lem1  25963  dvcnvrelem1  25978  itgpowd  26013  plyaddlem1  26174  plymullem1  26175  plycpn  26253  aalioulem3  26298  tayl0  26325  dvntaylp  26335  ulm2  26350  ulmdvlem1  26365  xrlimcnp  26934  dchrelbas2  27204  dchrghm  27223  dchrptlem1  27231  dchrptlem2  27232  iscgrgd  28585  iscgrglt  28586  trgcgrg  28587  tgcgr4  28603  motcgrg  28616  wrdupgr  29158  wrdumgr  29170  grporndm  30585  sspn  30811  fmptcof2  32735  fnpreimac  32749  curry2ima  32788  fpwrelmap  32812  indf1ofs  32948  swrdf1  33038  pmtrcnel  33171  pmtrcnel2  33172  pmtrcnelor  33173  wrdpmtrlast  33175  cycpmcl  33198  cycpmco2f1  33206  cycpmco2rn  33207  cycpmco2lem1  33208  cycpmco2lem2  33209  cycpmco2lem3  33210  cycpmco2lem4  33211  cycpmco2lem5  33212  cycpmco2lem6  33213  cycpmco2lem7  33214  cycpmco2  33215  cyc3co2  33222  cycpmconjv  33224  fxpgaval  33249  rmfsupp2  33320  elrgspnsubrunlem2  33330  rndrhmcl  33378  elrspunidl  33509  rhmimaidl  33513  1arithidomlem2  33617  1arithidom  33618  evls1dm  33642  evlextv  33707  esplymhp  33726  esplysply  33729  ply1degltdimlem  33779  fldextrspunlsp  33831  irngnzply1lem  33847  irngnzply1  33848  zarcmplem  34038  rhmpreimacnlem  34041  esumpcvgval  34235  ofcfval4  34262  measdivcst  34381  oms0  34454  omsmon  34455  omssubaddlem  34456  omssubadd  34457  carsgval  34460  omsmeas  34480  sitgclg  34499  eulerpartlemgu  34534  sseqfv2  34551  rrvdm  34603  ftc2re  34755  cvmliftmolem1  35475  cvmliftlem3  35481  cvmliftlem10  35488  cvmliftlem13  35490  cvmlift2lem9  35505  cvmlift3lem6  35518  cvmlift3lem7  35519  mclsax  35763  mclsppslem  35777  mclspps  35778  fwddifval  36356  fwddifnval  36357  weiunfrlem  36658  bj-finsumval0  37486  curunc  37799  itg2addnclem2  37869  ftc1anclem5  37894  ftc1anclem6  37895  ftc1anclem8  37897  sdclem2  37939  isbnd3  37981  ssbnd  37985  bnd2lem  37988  ismtyval  37997  grpokerinj  38090  rngosn3  38121  rngodm1dm2  38129  divrngcl  38154  isdrngo2  38155  sticksstones1  42396  aks5lem2  42437  evlselvlem  42825  mapfzcons2  42957  fnwe2lem2  43289  lmhmfgima  43322  wnefimgd  44398  binomcxplemnotnn0  44593  cncmpmax  45273  mullimcf  45865  limsuppnfdlem  45941  limsupvaluz  45948  climxrrelem  45989  climxrre  45990  liminfvalxr  46023  liminflimsupxrre  46057  xlimmnfvlem2  46073  xlimpnfvlem2  46077  xlimliminflimsup  46102  cncfuni  46126  cncficcgt0  46128  cncfioobd  46137  dvsinax  46153  itgperiod  46221  fvvolioof  46229  fvvolicof  46231  stoweidlem29  46269  fourierdlem20  46367  fourierdlem53  46399  fourierdlem63  46409  fourierdlem68  46414  fourierdlem82  46428  sge0sn  46619  sge0tsms  46620  sge0cl  46621  sge0isum  46667  ismeannd  46707  hoicvr  46788  dmovn  46844  hspmbl  46869  ovolval4lem1  46889  ovnovollem1  46896  ovnovollem2  46897  issmfd  46975  issmfdf  46977  cnfsmf  46980  issmfled  46997  issmfgtd  47001  smfsuplem1  47051  smfdivdmmbl2  47081  fcores  47309  f1cof1blem  47316  f1cof1b  47319  funfocofob  47320  rmsuppss  48612  itcovalendof  48911  ffvbr  49097  lmdran  49912  cmdlan  49913