Theorem fdmd 6708

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5647  ⟶wf 6523

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 6530  df-f 6531

This theorem is used by:  fssdmd  6716  fssdm  6717  foima  6789  focnvimacdmdm  6796  resdif  6834  fssrescdmd  7115  fmptco  7118  funfvima2d  7226  focdmex  7951  suppsnop  8173  onnseq  8330  fopwdom  9082  fodomfib  9298  intrnfi  9386  ordtypelem5  9494  ordtypelem6  9495  ordtypelem7  9496  ordtypelem8  9497  brwdomn0  9541  wdomtr  9547  fseqenlem2  10075  fin23lem30  10391  isf34lem5  10427  isf34lem7  10428  isf34lem6  10429  fin1a2lem7  10455  ttukeylem6  10563  fodomb  10576  pwxpndom2  10721  hashf1lem1  14567  wrddm  14633  ccatdmss  14694  swrdcl  14760  swrdf1  14766  cats1un  14837  repswswrd  14902  limsupgle  15611  limsupgre  15615  rlim  15629  rlimi  15647  lo1o1  15666  rlimuni  15684  o1co  15720  rlimcn1  15722  ruclem11  16375  1arith  17066  ramval  17147  0ram  17159  mrcuni  17756  homarcl2  18171  prfval  18334  pfxchn  18745  chnind  18756  chnccats1  18760  chnccat  18761  gsumval  18827  gsumval2  18836  mndpsuppss  18920  frmdss2  19020  ghmrn  19404  cntzmhm2  19517  gsumval3  20082  gsumzaddlem  20096  dmdprdd  20176  dprdres  20205  dprdf1  20210  dprd2da  20219  dmdprdsplit2lem  20222  dmdprdsplit2  20223  dmdprdsplit  20224  dprdsplit  20225  dpjidcl  20235  ablfac1eulem  20249  ablfac1eu  20250  ablfaclem2  20263  ablfac2  20266  crngrhmfo  20687  lmhmlsp  21285  rhmpreimaidl  21532  frlmsslsp  22063  f1lindf  22089  mattpostpos  22730  iinopn  23181  lmbrf  23539  cnntri  23550  cnclsi  23551  lmcnp  23583  cnt0  23625  cnt1  23629  cnhaus  23633  cncmp  23671  connima  23704  1stcfb  23724  1stccnp  23742  1stckgenlem  23833  kgencn3  23838  txcnpi  23888  txcnp  23900  prdstps  23909  xkohaus  23933  xkoco2cn  23938  qtopeu  23996  hmeores  24051  fmfnfmlem2  24235  fmfnfmlem4  24237  fmfnfm  24238  lmflf  24285  txflf  24286  cnextfval  24342  cnextcn  24347  clssubg  24389  ghmcnp  24395  qustgplem  24401  tsmsval  24411  ucncn  24564  xmetdmdm  24615  metn0  24640  tmsval  24761  metustid  24834  metustexhalf  24836  metustfbas  24837  isngp2  24877  evth  25241  lmmbrf  25544  iscfil2  25548  caufval  25557  iscau2  25559  caucfil  25565  ovollb2  25771  ovolunlem1a  25778  ovoliunlem1  25784  ovoliun2  25788  ioombl1lem4  25843  uniioombllem1  25863  uniioombllem2  25865  uniioombllem6  25870  mbfconstlem  25909  ismbfcn  25911  mbfmulc2lem  25929  mbfmulc2re  25930  cncombf  25940  mbfaddlem  25942  mbflimsup  25948  i1f0rn  25964  itg1addlem5  25982  itg1climres  25996  mbfmullem2  26006  limcfval  26153  limcdif  26157  ellimc2  26158  ellimc3  26160  limccnp  26172  dvfval  26178  cpnord  26216  cpnres  26218  dvcmul  26225  dvcmulf  26226  dvexp  26234  dvgt0lem1  26283  dvcnvrelem1  26298  itgpowd  26331  plyaddlem1  26493  plymullem1  26494  plycpn  26573  rnplynfin  26593  plyconz  26594  aalioulem3  26624  tayl0  26652  dvntaylp  26661  ulm2  26675  ulmdvlem1  26690  xrlimcnp  27259  dchrelbas2  27527  dchrghm  27546  dchrptlem1  27554  dchrptlem2  27555  iscgrgd  28909  iscgrglt  28910  trgcgrg  28911  tgcgr4  28927  motcgrg  28940  wrdupgr  29596  wrdumgr  29608  grporndm  31045  sspn  31271  fmptcof2  33184  fnpreimac  33197  curry2ima  33235  fpwrelmap  33258  indf1ofs  33366  pmtrcnel  33583  pmtrcnel2  33584  pmtrcnelor  33585  wrdpmtrlast  33587  cycpmcl  33610  cycpmco2f1  33618  cycpmco2rn  33619  cycpmco2lem1  33620  cycpmco2lem2  33621  cycpmco2lem3  33622  cycpmco2lem4  33623  cycpmco2lem5  33624  cycpmco2lem6  33625  cycpmco2lem7  33626  cycpmco2  33627  cyc3co2  33634  cycpmconjv  33636  fxpgaval  33661  rmfsupp2  33731  elrgspnsubrunlem2  33742  rndrhmcl  33791  elrspunidl  33911  rhmimaidl  33915  1arithidomlem2  34001  1arithidom  34002  evls1dm  34026  selvascl  34082  evlextv  34107  esplymhp  34133  esplysply  34136  esplyfval1  34138  ply1degltdimlem  34187  fldextrspunlsp  34239  irngnzply1lem  34255  irngnzply1  34256  zarcmplem  34446  rhmpreimacnlem  34449  esumpcvgval  34643  ofcfval4  34670  measdivcst  34790  oms0  34863  omsmon  34864  omssubaddlem  34865  omssubadd  34866  carsgval  34869  omsmeas  34889  sitgclg  34908  eulerpartlemgu  34943  sseqfv2  34960  rrvdm  35012  ftc2re  35161  cvmliftmolem1  35967  cvmliftlem3  35973  cvmliftlem10  35980  cvmliftlem13  35982  cvmlift2lem9  35997  cvmlift3lem6  36010  cvmlift3lem7  36011  mclsax  36255  mclsppslem  36269  mclspps  36270  fwddifval  36849  fwddifnval  36850  weiunfrlem  37174  bj-finsumval0  38126  curunc  38445  itg2addnclem2  38510  ftc1anclem5  38535  ftc1anclem6  38536  ftc1anclem8  38538  sdclem2  38596  isbnd3  38638  ssbnd  38642  bnd2lem  38645  ismtyval  38654  grpokerinj  38747  rngosn3  38778  rngodm1dm2  38786  divrngcl  38811  isdrngo2  38812  sticksstones1  43116  aks5lem2  43157  evlselvlem  43538  mapfzcons2  43668  fnwe2lem2  43996  lmhmfgima  44029  wnefimgd  45105  binomcxplemnotnn0  45284  cncmpmax  45970  mullimcf  46557  limsuppnfdlem  46633  limsupvaluz  46640  climxrrelem  46681  climxrre  46682  liminfvalxr  46715  liminflimsupxrre  46749  xlimmnfvlem2  46765  xlimpnfvlem2  46769  xlimliminflimsup  46794  cncfuni  46818  cncficcgt0  46820  cncfioobd  46829  dvsinax  46845  itgperiod  46913  fvvolioof  46921  fvvolicof  46923  stoweidlem29  46961  fourierdlem20  47059  fourierdlem48  47086  fourierdlem49  47087  fourierdlem53  47091  fourierdlem63  47101  fourierdlem68  47106  fourierdlem82  47120  fourierdlem113  47151  sge0sn  47311  sge0tsms  47312  sge0cl  47313  sge0isum  47359  ismeannd  47399  hoicvr  47480  dmovn  47536  hspmbl  47561  ovolval4lem1  47581  ovnovollem1  47588  ovnovollem2  47589  issmfd  47667  issmfdf  47669  cnfsmf  47672  issmfled  47689  issmfgtd  47693  smfsuplem1  47743  smfdivdmmbl2  47773  tmachlem-agreesn  47879  fcores  48059  f1cof1blem  48066  f1cof1b  48069  funfocofob  48070  rmsuppss  49404  itcovalendof  49703  ffvbr  49888  lmdran  50701  cmdlan  50702