Theorem fdmd 6667

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5620  ⟶wf 6483

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

This theorem is referenced by:  fssdmd  6675  fssdm  6676  foima  6746  focnvimacdmdm  6753  resdif  6790  fssrescdmd  7068  fmptco  7071  funfvima2d  7176  focdmex  7898  suppsnop  8117  onnseq  8273  fopwdom  9012  fodomfib  9228  fodomfibOLD  9230  intrnfi  9318  ordtypelem5  9426  ordtypelem6  9427  ordtypelem7  9428  ordtypelem8  9429  brwdomn0  9473  wdomtr  9479  fseqenlem2  9936  fin23lem30  10253  isf34lem5  10289  isf34lem7  10290  isf34lem6  10291  fin1a2lem7  10317  ttukeylem6  10425  fodomb  10437  pwxpndom2  10577  hashf1lem1  14406  wrddm  14472  ccatdmss  14533  swrdcl  14597  cats1un  14672  repswswrd  14735  limsupgle  15428  limsupgre  15432  rlim  15446  rlimi  15464  lo1o1  15483  rlimuni  15501  o1co  15537  rlimcn1  15539  ruclem11  16196  1arith  16887  ramval  16968  0ram  16980  mrcuni  17576  homarcl2  17991  prfval  18154  pfxchn  18565  chnind  18576  chnccats1  18580  chnccat  18581  gsumval  18634  gsumval2  18643  mndpsuppss  18722  frmdss2  18820  ghmrn  19193  cntzmhm2  19306  gsumval3  19871  gsumzaddlem  19885  dmdprdd  19965  dprdres  19994  dprdf1  19999  dprd2da  20008  dmdprdsplit2lem  20011  dmdprdsplit2  20012  dmdprdsplit  20013  dprdsplit  20014  dpjidcl  20024  ablfac1eulem  20038  ablfac1eu  20039  ablfaclem2  20052  ablfac2  20055  lmhmlsp  21033  rhmpreimaidl  21264  frlmsslsp  21765  f1lindf  21791  mattpostpos  22407  iinopn  22855  lmbrf  23213  cnntri  23224  cnclsi  23225  lmcnp  23257  cnt0  23299  cnt1  23303  cnhaus  23307  cncmp  23345  connima  23378  1stcfb  23398  1stccnp  23415  1stckgenlem  23506  kgencn3  23511  txcnpi  23561  txcnp  23573  prdstps  23582  xkohaus  23606  xkoco2cn  23611  qtopeu  23669  hmeores  23724  fmfnfmlem2  23908  fmfnfmlem4  23910  fmfnfm  23911  lmflf  23958  txflf  23959  cnextfval  24015  cnextcn  24020  clssubg  24062  ghmcnp  24068  qustgplem  24074  tsmsval  24084  ucncn  24237  xmetdmdm  24288  metn0  24313  tmsval  24434  metustid  24507  metustexhalf  24509  metustfbas  24510  isngp2  24550  evth  24914  lmmbrf  25217  iscfil2  25221  caufval  25230  iscau2  25232  caucfil  25238  ovollb2  25444  ovolunlem1a  25451  ovoliunlem1  25457  ovoliun2  25461  ioombl1lem4  25516  uniioombllem1  25536  uniioombllem2  25538  uniioombllem6  25543  mbfconstlem  25582  ismbfcn  25584  mbfmulc2lem  25602  mbfmulc2re  25603  cncombf  25613  mbfaddlem  25615  mbflimsup  25621  i1f0rn  25637  itg1addlem5  25655  itg1climres  25669  mbfmullem2  25679  limcfval  25827  limcdif  25831  ellimc2  25832  ellimc3  25834  limccnp  25846  dvfval  25852  cpnord  25890  cpnres  25892  dvcmul  25899  dvcmulf  25900  dvexp  25908  dvgt0lem1  25957  dvcnvrelem1  25972  itgpowd  26005  plyaddlem1  26166  plymullem1  26167  plycpn  26243  aalioulem3  26288  tayl0  26315  dvntaylp  26324  ulm2  26338  ulmdvlem1  26353  xrlimcnp  26920  dchrelbas2  27188  dchrghm  27207  dchrptlem1  27215  dchrptlem2  27216  iscgrgd  28569  iscgrglt  28570  trgcgrg  28571  tgcgr4  28587  motcgrg  28600  wrdupgr  29142  wrdumgr  29154  grporndm  30569  sspn  30795  fmptcof2  32718  fnpreimac  32731  curry2ima  32770  fpwrelmap  32794  indf1ofs  32914  swrdf1  33004  pmtrcnel  33138  pmtrcnel2  33139  pmtrcnelor  33140  wrdpmtrlast  33142  cycpmcl  33165  cycpmco2f1  33173  cycpmco2rn  33174  cycpmco2lem1  33175  cycpmco2lem2  33176  cycpmco2lem3  33177  cycpmco2lem4  33178  cycpmco2lem5  33179  cycpmco2lem6  33180  cycpmco2lem7  33181  cycpmco2  33182  cyc3co2  33189  cycpmconjv  33191  fxpgaval  33216  rmfsupp2  33287  elrgspnsubrunlem2  33297  rndrhmcl  33345  elrspunidl  33476  rhmimaidl  33480  1arithidomlem2  33584  1arithidom  33585  evls1dm  33609  evlextv  33674  esplymhp  33700  esplysply  33703  esplyfval1  33705  ply1degltdimlem  33754  fldextrspunlsp  33806  irngnzply1lem  33822  irngnzply1  33823  zarcmplem  34013  rhmpreimacnlem  34016  esumpcvgval  34210  ofcfval4  34237  measdivcst  34356  oms0  34429  omsmon  34430  omssubaddlem  34431  omssubadd  34432  carsgval  34435  omsmeas  34455  sitgclg  34474  eulerpartlemgu  34509  sseqfv2  34526  rrvdm  34578  ftc2re  34730  cvmliftmolem1  35451  cvmliftlem3  35457  cvmliftlem10  35464  cvmliftlem13  35466  cvmlift2lem9  35481  cvmlift3lem6  35494  cvmlift3lem7  35495  mclsax  35739  mclsppslem  35753  mclspps  35754  fwddifval  36332  fwddifnval  36333  weiunfrlem  36634  bj-finsumval0  37587  curunc  37911  itg2addnclem2  37981  ftc1anclem5  38006  ftc1anclem6  38007  ftc1anclem8  38009  sdclem2  38051  isbnd3  38093  ssbnd  38097  bnd2lem  38100  ismtyval  38109  grpokerinj  38202  rngosn3  38233  rngodm1dm2  38241  divrngcl  38266  isdrngo2  38267  sticksstones1  42573  aks5lem2  42614  evlselvlem  43007  mapfzcons2  43139  fnwe2lem2  43467  lmhmfgima  43500  wnefimgd  44576  binomcxplemnotnn0  44771  cncmpmax  45451  mullimcf  46041  limsuppnfdlem  46117  limsupvaluz  46124  climxrrelem  46165  climxrre  46166  liminfvalxr  46199  liminflimsupxrre  46233  xlimmnfvlem2  46249  xlimpnfvlem2  46253  xlimliminflimsup  46278  cncfuni  46302  cncficcgt0  46304  cncfioobd  46313  dvsinax  46329  itgperiod  46397  fvvolioof  46405  fvvolicof  46407  stoweidlem29  46445  fourierdlem20  46543  fourierdlem53  46575  fourierdlem63  46585  fourierdlem68  46590  fourierdlem82  46604  sge0sn  46795  sge0tsms  46796  sge0cl  46797  sge0isum  46843  ismeannd  46883  hoicvr  46964  dmovn  47020  hspmbl  47045  ovolval4lem1  47065  ovnovollem1  47072  ovnovollem2  47073  issmfd  47151  issmfdf  47153  cnfsmf  47156  issmfled  47173  issmfgtd  47177  smfsuplem1  47227  smfdivdmmbl2  47257  fcores  47503  f1cof1blem  47510  f1cof1b  47513  funfocofob  47514  rmsuppss  48834  itcovalendof  49133  ffvbr  49319  lmdran  50134  cmdlan  50135