Theorem fdmd 6716

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5654  ⟶wf 6527

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 6534  df-f 6535

This theorem is referenced by:  fssdmd  6724  fssdm  6725  foima  6795  focnvimacdmdm  6802  resdif  6839  fssrescdmd  7116  fmptco  7119  funfvima2d  7224  focdmex  7954  suppsnop  8177  onnseq  8358  fopwdom  9094  fodomfib  9341  fodomfibOLD  9343  intrnfi  9428  ordtypelem5  9536  ordtypelem6  9537  ordtypelem7  9538  ordtypelem8  9539  brwdomn0  9583  wdomtr  9589  fseqenlem2  10039  fin23lem30  10356  isf34lem5  10392  isf34lem7  10393  isf34lem6  10394  fin1a2lem7  10420  ttukeylem6  10528  fodomb  10540  pwxpndom2  10679  hashf1lem1  14473  wrddm  14539  swrdcl  14663  cats1un  14739  repswswrd  14802  limsupgle  15493  limsupgre  15497  rlim  15511  rlimi  15529  lo1o1  15548  rlimuni  15566  o1co  15602  rlimcn1  15604  ruclem11  16258  1arith  16947  ramval  17028  0ram  17040  mrcuni  17633  homarcl2  18048  prfval  18211  gsumval  18655  gsumval2  18664  mndpsuppss  18743  frmdss2  18841  ghmrn  19212  cntzmhm2  19325  gsumval3  19888  gsumzaddlem  19902  dmdprdd  19982  dprdres  20011  dprdf1  20016  dprd2da  20025  dmdprdsplit2lem  20028  dmdprdsplit2  20029  dmdprdsplit  20030  dprdsplit  20031  dpjidcl  20041  ablfac1eulem  20055  ablfac1eu  20056  ablfaclem2  20069  ablfac2  20072  lmhmlsp  21007  rhmpreimaidl  21238  frlmsslsp  21756  f1lindf  21782  mattpostpos  22392  iinopn  22840  lmbrf  23198  cnntri  23209  cnclsi  23210  lmcnp  23242  cnt0  23284  cnt1  23288  cnhaus  23292  cncmp  23330  connima  23363  1stcfb  23383  1stccnp  23400  1stckgenlem  23491  kgencn3  23496  txcnpi  23546  txcnp  23558  prdstps  23567  xkohaus  23591  xkoco2cn  23596  qtopeu  23654  hmeores  23709  fmfnfmlem2  23893  fmfnfmlem4  23895  fmfnfm  23896  lmflf  23943  txflf  23944  cnextfval  24000  cnextcn  24005  clssubg  24047  ghmcnp  24053  qustgplem  24059  tsmsval  24069  ucncn  24223  xmetdmdm  24274  metn0  24299  tmsval  24420  metustid  24493  metustexhalf  24495  metustfbas  24496  isngp2  24536  evth  24909  lmmbrf  25214  iscfil2  25218  caufval  25227  iscau2  25229  caucfil  25235  ovollb2  25442  ovolunlem1a  25449  ovoliunlem1  25455  ovoliun2  25459  ioombl1lem4  25514  uniioombllem1  25534  uniioombllem2  25536  uniioombllem6  25541  mbfconstlem  25580  ismbfcn  25582  mbfmulc2lem  25600  mbfmulc2re  25601  cncombf  25611  mbfaddlem  25613  mbflimsup  25619  i1f0rn  25635  itg1addlem5  25653  itg1climres  25667  mbfmullem2  25677  limcfval  25825  limcdif  25829  ellimc2  25830  ellimc3  25832  limccnp  25844  dvfval  25850  cpnord  25889  cpnres  25891  dvcmul  25899  dvcmulf  25900  dvexp  25909  dvgt0lem1  25959  dvcnvrelem1  25974  itgpowd  26009  plyaddlem1  26170  plymullem1  26171  plycpn  26249  aalioulem3  26294  tayl0  26321  dvntaylp  26331  ulm2  26346  ulmdvlem1  26361  xrlimcnp  26930  dchrelbas2  27200  dchrghm  27219  dchrptlem1  27227  dchrptlem2  27228  iscgrgd  28492  iscgrglt  28493  trgcgrg  28494  tgcgr4  28510  motcgrg  28523  wrdupgr  29064  wrdumgr  29076  grporndm  30491  sspn  30717  fmptcof2  32635  fnpreimac  32649  curry2ima  32686  fpwrelmap  32710  indf1ofs  32843  ccatdmss  32925  swrdf1  32932  pfxchn  32989  chnind  32991  chnccats1  32995  pmtrcnel  33100  pmtrcnel2  33101  pmtrcnelor  33102  wrdpmtrlast  33104  cycpmcl  33127  cycpmco2f1  33135  cycpmco2rn  33136  cycpmco2lem1  33137  cycpmco2lem2  33138  cycpmco2lem3  33139  cycpmco2lem4  33140  cycpmco2lem5  33141  cycpmco2lem6  33142  cycpmco2lem7  33143  cycpmco2  33144  cyc3co2  33151  cycpmconjv  33153  rmfsupp2  33233  elrgspnsubrunlem2  33243  rndrhmcl  33290  elrspunidl  33443  rhmimaidl  33447  1arithidomlem2  33551  1arithidom  33552  evls1dm  33574  ply1degltdimlem  33662  fldextrspunlsp  33715  irngnzply1lem  33731  irngnzply1  33732  zarcmplem  33912  rhmpreimacnlem  33915  esumpcvgval  34109  ofcfval4  34136  measdivcst  34255  oms0  34329  omsmon  34330  omssubaddlem  34331  omssubadd  34332  carsgval  34335  omsmeas  34355  sitgclg  34374  eulerpartlemgu  34409  sseqfv2  34426  rrvdm  34478  ftc2re  34630  cvmliftmolem1  35303  cvmliftlem3  35309  cvmliftlem10  35316  cvmliftlem13  35318  cvmlift2lem9  35333  cvmlift3lem6  35346  cvmlift3lem7  35347  mclsax  35591  mclsppslem  35605  mclspps  35606  fwddifval  36180  fwddifnval  36181  weiunfrlem  36482  bj-finsumval0  37303  curunc  37626  itg2addnclem2  37696  ftc1anclem5  37721  ftc1anclem6  37722  ftc1anclem8  37724  sdclem2  37766  isbnd3  37808  ssbnd  37812  bnd2lem  37815  ismtyval  37824  grpokerinj  37917  rngosn3  37948  rngodm1dm2  37956  divrngcl  37981  isdrngo2  37982  sticksstones1  42159  aks5lem2  42200  evlselvlem  42609  mapfzcons2  42742  fnwe2lem2  43075  lmhmfgima  43108  wnefimgd  44185  binomcxplemnotnn0  44380  cncmpmax  45056  mullimcf  45652  limsuppnfdlem  45730  limsupvaluz  45737  climxrrelem  45778  climxrre  45779  liminfvalxr  45812  liminflimsupxrre  45846  xlimmnfvlem2  45862  xlimpnfvlem2  45866  xlimliminflimsup  45891  cncfuni  45915  cncficcgt0  45917  cncfioobd  45926  dvsinax  45942  itgperiod  46010  fvvolioof  46018  fvvolicof  46020  stoweidlem29  46058  fourierdlem20  46156  fourierdlem53  46188  fourierdlem63  46198  fourierdlem68  46203  fourierdlem82  46217  sge0sn  46408  sge0tsms  46409  sge0cl  46410  sge0isum  46456  ismeannd  46496  hoicvr  46577  dmovn  46633  hspmbl  46658  ovolval4lem1  46678  ovnovollem1  46685  ovnovollem2  46686  issmfd  46764  issmfdf  46766  cnfsmf  46769  issmfled  46786  issmfgtd  46790  smfsuplem1  46840  smfdivdmmbl2  46870  fcores  47096  f1cof1blem  47103  f1cof1b  47106  funfocofob  47107  rmsuppss  48345  itcovalendof  48649