Theorem fdmd 6720

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  dom cdm 5650  ⟶wf 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6541  df-f 6542

This theorem is used by:  fssdmd  6728  fssdm  6729  foima  6801  focnvimacdmdm  6808  resdif  6846  fssrescdmd  7127  fmptco  7130  funfvima2d  7238  focdmex  7968  suppsnop  8195  onnseq  8352  fopwdom  9104  fodomfib  9320  intrnfi  9408  ordtypelem5  9516  ordtypelem6  9517  ordtypelem7  9518  ordtypelem8  9519  brwdomn0  9563  wdomtr  9569  fseqenlem2  10104  fin23lem30  10420  isf34lem5  10456  isf34lem7  10457  isf34lem6  10458  fin1a2lem7  10484  ttukeylem6  10592  fodomb  10605  pwxpndom2  10750  hashf1lem1  14600  wrddm  14666  ccatdmss  14727  swrdcl  14793  swrdf1  14799  cats1un  14870  repswswrd  14935  limsupgle  15644  limsupgre  15648  rlim  15662  rlimi  15680  lo1o1  15699  rlimuni  15717  o1co  15753  rlimcn1  15755  ruclem11  16408  1arith  17105  ramval  17186  0ram  17198  mrcuni  17795  homarcl2  18210  prfval  18373  pfxchn  18784  chnind  18795  chnccats1  18799  chnccat  18800  gsumval  18866  gsumval2  18875  mndpsuppss  18959  frmdss2  19059  ghmrn  19443  cntzmhm2  19556  gsumval3  20121  gsumzaddlem  20135  dmdprdd  20215  dprdres  20244  dprdf1  20249  dprd2da  20258  dmdprdsplit2lem  20261  dmdprdsplit2  20262  dmdprdsplit  20263  dprdsplit  20264  dpjidcl  20274  ablfac1eulem  20288  ablfac1eu  20289  ablfaclem2  20302  ablfac2  20305  crngrhmfo  20726  lmhmlsp  21324  rhmpreimaidl  21571  frlmsslsp  22102  f1lindf  22128  mattpostpos  22769  iinopn  23220  lmbrf  23578  cnntri  23589  cnclsi  23590  lmcnp  23622  cnt0  23664  cnt1  23668  cnhaus  23672  cncmp  23710  connima  23743  1stcfb  23763  1stccnp  23781  1stckgenlem  23872  kgencn3  23877  txcnpi  23927  txcnp  23939  prdstps  23948  xkohaus  23972  xkoco2cn  23977  qtopeu  24035  hmeores  24090  fmfnfmlem2  24274  fmfnfmlem4  24276  fmfnfm  24277  lmflf  24324  txflf  24325  cnextfval  24381  cnextcn  24386  clssubg  24428  ghmcnp  24434  qustgplem  24440  tsmsval  24450  ucncn  24603  xmetdmdm  24654  metn0  24679  tmsval  24800  metustid  24873  metustexhalf  24875  metustfbas  24876  isngp2  24916  evth  25280  lmmbrf  25583  iscfil2  25587  caufval  25596  iscau2  25598  caucfil  25604  ovollb2  25810  ovolunlem1a  25817  ovoliunlem1  25823  ovoliun2  25827  ioombl1lem4  25882  uniioombllem1  25902  uniioombllem2  25904  uniioombllem6  25909  mbfconstlem  25948  ismbfcn  25950  mbfmulc2lem  25968  mbfmulc2re  25969  cncombf  25979  mbfaddlem  25981  mbflimsup  25987  i1f0rn  26003  itg1addlem5  26021  itg1climres  26035  mbfmullem2  26045  limcfval  26192  limcdif  26196  ellimc2  26197  ellimc3  26199  limccnp  26211  dvfval  26217  cpnord  26255  cpnres  26257  dvcmul  26264  dvcmulf  26265  dvexp  26273  dvgt0lem1  26322  dvcnvrelem1  26337  itgpowd  26370  plyaddlem1  26532  plymullem1  26533  plycpn  26610  rnplynfin  26630  plyconz  26631  aalioulem3  26661  tayl0  26689  dvntaylp  26698  ulm2  26712  ulmdvlem1  26727  xrlimcnp  27296  dchrelbas2  27564  dchrghm  27583  dchrptlem1  27591  dchrptlem2  27592  iscgrgd  28976  iscgrglt  28977  trgcgrg  28978  tgcgr4  28994  motcgrg  29007  wrdupgr  29663  wrdumgr  29675  grporndm  31112  sspn  31338  fmptcof2  33293  fnpreimac  33306  curry2ima  33344  fpwrelmap  33367  indf1ofs  33475  pmtrcnel  33692  pmtrcnel2  33693  pmtrcnelor  33694  wrdpmtrlast  33696  cycpmcl  33719  cycpmco2f1  33727  cycpmco2rn  33728  cycpmco2lem1  33729  cycpmco2lem2  33730  cycpmco2lem3  33731  cycpmco2lem4  33732  cycpmco2lem5  33733  cycpmco2lem6  33734  cycpmco2lem7  33735  cycpmco2  33736  cyc3co2  33743  cycpmconjv  33745  fxpgaval  33770  rmfsupp2  33840  elrgspnsubrunlem2  33851  rndrhmcl  33900  elrspunidl  34020  rhmimaidl  34024  1arithidomlem2  34110  1arithidom  34111  evls1dm  34135  selvascl  34191  evlextv  34216  esplymhp  34242  esplysply  34245  esplyfval1  34247  ply1degltdimlem  34296  fldextrspunlsp  34348  irngnzply1lem  34364  irngnzply1  34365  zarcmplem  34555  rhmpreimacnlem  34558  esumpcvgval  34752  ofcfval4  34779  measdivcst  34899  oms0  34971  omsmon  34972  omssubaddlem  34973  omssubadd  34974  carsgval  34977  omsmeas  34997  sitgclg  35016  eulerpartlemgu  35051  sseqfv2  35068  rrvdm  35120  ftc2re  35269  cvmliftmolem1  36088  cvmliftlem3  36094  cvmliftlem10  36101  cvmliftlem13  36103  cvmlift2lem9  36118  cvmlift3lem6  36131  cvmlift3lem7  36132  mclsax  36376  mclsppslem  36390  mclspps  36391  fwddifval  36969  fwddifnval  36970  weiunfrlem  37294  bj-finsumval0  38249  curunc  38568  itg2addnclem2  38633  ftc1anclem5  38658  ftc1anclem6  38659  ftc1anclem8  38661  sdclem2  38719  isbnd3  38761  ssbnd  38765  bnd2lem  38768  ismtyval  38777  grpokerinj  38870  rngosn3  38901  rngodm1dm2  38909  divrngcl  38934  isdrngo2  38935  sticksstones1  43239  aks5lem2  43280  evlselvlem  43659  mapfzcons2  43773  lmhmfgima  44129  wnefimgd  45204  binomcxplemnotnn0  45383  cncmpmax  46092  mullimcf  46678  limsuppnfdlem  46754  limsupvaluz  46761  climxrrelem  46802  climxrre  46803  liminfvalxr  46836  liminflimsupxrre  46870  xlimmnfvlem2  46886  xlimpnfvlem2  46890  xlimliminflimsup  46915  cncfuni  46939  cncficcgt0  46941  cncfioobd  46950  dvsinax  46966  itgperiod  47034  fvvolioof  47042  fvvolicof  47044  stoweidlem29  47082  fourierdlem20  47180  fourierdlem48  47207  fourierdlem49  47208  fourierdlem53  47212  fourierdlem63  47222  fourierdlem68  47227  fourierdlem82  47241  fourierdlem113  47272  sge0sn  47432  sge0tsms  47433  sge0cl  47434  sge0isum  47480  ismeannd  47520  hoicvr  47601  dmovn  47657  hspmbl  47682  ovolval4lem1  47702  ovnovollem1  47709  ovnovollem2  47710  issmfd  47788  issmfdf  47790  cnfsmf  47793  issmfled  47810  issmfgtd  47814  smfsuplem1  47864  smfdivdmmbl2  47894  tmachlem-agreesn  48000  fcores  48180  f1cof1blem  48187  f1cof1b  48190  funfocofob  48191  rmsuppss  49525  itcovalendof  49824  ffvbr  50009  lmdran  50822  cmdlan  50823