Theorem fdmd 6666

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5623  ⟶wf 6482

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 6489  df-f 6490

This theorem is referenced by:  fssdmd  6674  fssdm  6675  foima  6745  focnvimacdmdm  6752  resdif  6789  fssrescdmd  7064  fmptco  7067  funfvima2d  7172  focdmex  7898  suppsnop  8118  onnseq  8274  fopwdom  9009  fodomfib  9238  fodomfibOLD  9240  intrnfi  9325  ordtypelem5  9433  ordtypelem6  9434  ordtypelem7  9435  ordtypelem8  9436  brwdomn0  9480  wdomtr  9486  fseqenlem2  9938  fin23lem30  10255  isf34lem5  10291  isf34lem7  10292  isf34lem6  10293  fin1a2lem7  10319  ttukeylem6  10427  fodomb  10439  pwxpndom2  10578  hashf1lem1  14380  wrddm  14446  swrdcl  14570  cats1un  14645  repswswrd  14708  limsupgle  15402  limsupgre  15406  rlim  15420  rlimi  15438  lo1o1  15457  rlimuni  15475  o1co  15511  rlimcn1  15513  ruclem11  16167  1arith  16857  ramval  16938  0ram  16950  mrcuni  17545  homarcl2  17960  prfval  18123  gsumval  18569  gsumval2  18578  mndpsuppss  18657  frmdss2  18755  ghmrn  19126  cntzmhm2  19239  gsumval3  19804  gsumzaddlem  19818  dmdprdd  19898  dprdres  19927  dprdf1  19932  dprd2da  19941  dmdprdsplit2lem  19944  dmdprdsplit2  19945  dmdprdsplit  19946  dprdsplit  19947  dpjidcl  19957  ablfac1eulem  19971  ablfac1eu  19972  ablfaclem2  19985  ablfac2  19988  lmhmlsp  20971  rhmpreimaidl  21202  frlmsslsp  21721  f1lindf  21747  mattpostpos  22357  iinopn  22805  lmbrf  23163  cnntri  23174  cnclsi  23175  lmcnp  23207  cnt0  23249  cnt1  23253  cnhaus  23257  cncmp  23295  connima  23328  1stcfb  23348  1stccnp  23365  1stckgenlem  23456  kgencn3  23461  txcnpi  23511  txcnp  23523  prdstps  23532  xkohaus  23556  xkoco2cn  23561  qtopeu  23619  hmeores  23674  fmfnfmlem2  23858  fmfnfmlem4  23860  fmfnfm  23861  lmflf  23908  txflf  23909  cnextfval  23965  cnextcn  23970  clssubg  24012  ghmcnp  24018  qustgplem  24024  tsmsval  24034  ucncn  24188  xmetdmdm  24239  metn0  24264  tmsval  24385  metustid  24458  metustexhalf  24460  metustfbas  24461  isngp2  24501  evth  24874  lmmbrf  25178  iscfil2  25182  caufval  25191  iscau2  25193  caucfil  25199  ovollb2  25406  ovolunlem1a  25413  ovoliunlem1  25419  ovoliun2  25423  ioombl1lem4  25478  uniioombllem1  25498  uniioombllem2  25500  uniioombllem6  25505  mbfconstlem  25544  ismbfcn  25546  mbfmulc2lem  25564  mbfmulc2re  25565  cncombf  25575  mbfaddlem  25577  mbflimsup  25583  i1f0rn  25599  itg1addlem5  25617  itg1climres  25631  mbfmullem2  25641  limcfval  25789  limcdif  25793  ellimc2  25794  ellimc3  25796  limccnp  25808  dvfval  25814  cpnord  25853  cpnres  25855  dvcmul  25863  dvcmulf  25864  dvexp  25873  dvgt0lem1  25923  dvcnvrelem1  25938  itgpowd  25973  plyaddlem1  26134  plymullem1  26135  plycpn  26213  aalioulem3  26258  tayl0  26285  dvntaylp  26295  ulm2  26310  ulmdvlem1  26325  xrlimcnp  26894  dchrelbas2  27164  dchrghm  27183  dchrptlem1  27191  dchrptlem2  27192  iscgrgd  28476  iscgrglt  28477  trgcgrg  28478  tgcgr4  28494  motcgrg  28507  wrdupgr  29048  wrdumgr  29060  grporndm  30472  sspn  30698  fmptcof2  32614  fnpreimac  32628  curry2ima  32665  fpwrelmap  32689  indf1ofs  32822  ccatdmss  32904  swrdf1  32911  pfxchn  32964  chnind  32966  chnccats1  32970  pmtrcnel  33044  pmtrcnel2  33045  pmtrcnelor  33046  wrdpmtrlast  33048  cycpmcl  33071  cycpmco2f1  33079  cycpmco2rn  33080  cycpmco2lem1  33081  cycpmco2lem2  33082  cycpmco2lem3  33083  cycpmco2lem4  33084  cycpmco2lem5  33085  cycpmco2lem6  33086  cycpmco2lem7  33087  cycpmco2  33088  cyc3co2  33095  cycpmconjv  33097  fxpgaval  33122  rmfsupp2  33188  elrgspnsubrunlem2  33198  rndrhmcl  33245  elrspunidl  33375  rhmimaidl  33379  1arithidomlem2  33483  1arithidom  33484  evls1dm  33506  ply1degltdimlem  33594  fldextrspunlsp  33645  irngnzply1lem  33661  irngnzply1  33662  zarcmplem  33847  rhmpreimacnlem  33850  esumpcvgval  34044  ofcfval4  34071  measdivcst  34190  oms0  34264  omsmon  34265  omssubaddlem  34266  omssubadd  34267  carsgval  34270  omsmeas  34290  sitgclg  34309  eulerpartlemgu  34344  sseqfv2  34361  rrvdm  34413  ftc2re  34565  cvmliftmolem1  35253  cvmliftlem3  35259  cvmliftlem10  35266  cvmliftlem13  35268  cvmlift2lem9  35283  cvmlift3lem6  35296  cvmlift3lem7  35297  mclsax  35541  mclsppslem  35555  mclspps  35556  fwddifval  36135  fwddifnval  36136  weiunfrlem  36437  bj-finsumval0  37258  curunc  37581  itg2addnclem2  37651  ftc1anclem5  37676  ftc1anclem6  37677  ftc1anclem8  37679  sdclem2  37721  isbnd3  37763  ssbnd  37767  bnd2lem  37770  ismtyval  37779  grpokerinj  37872  rngosn3  37903  rngodm1dm2  37911  divrngcl  37936  isdrngo2  37937  sticksstones1  42119  aks5lem2  42160  evlselvlem  42559  mapfzcons2  42692  fnwe2lem2  43024  lmhmfgima  43057  wnefimgd  44134  binomcxplemnotnn0  44329  cncmpmax  45010  mullimcf  45605  limsuppnfdlem  45683  limsupvaluz  45690  climxrrelem  45731  climxrre  45732  liminfvalxr  45765  liminflimsupxrre  45799  xlimmnfvlem2  45815  xlimpnfvlem2  45819  xlimliminflimsup  45844  cncfuni  45868  cncficcgt0  45870  cncfioobd  45879  dvsinax  45895  itgperiod  45963  fvvolioof  45971  fvvolicof  45973  stoweidlem29  46011  fourierdlem20  46109  fourierdlem53  46141  fourierdlem63  46151  fourierdlem68  46156  fourierdlem82  46170  sge0sn  46361  sge0tsms  46362  sge0cl  46363  sge0isum  46409  ismeannd  46449  hoicvr  46530  dmovn  46586  hspmbl  46611  ovolval4lem1  46631  ovnovollem1  46638  ovnovollem2  46639  issmfd  46717  issmfdf  46719  cnfsmf  46722  issmfled  46739  issmfgtd  46743  smfsuplem1  46793  smfdivdmmbl2  46823  fcores  47052  f1cof1blem  47059  f1cof1b  47062  funfocofob  47063  rmsuppss  48342  itcovalendof  48642  ffvbr  48828  lmdran  49644  cmdlan  49645