Theorem fdmd 6717

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

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

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 6540  df-f 6541

This theorem is used by:  fssdmd  6725  fssdm  6726  foima  6798  focnvimacdmdm  6805  resdif  6843  fssrescdmd  7123  fmptco  7126  funfvima2d  7234  focdmex  7956  suppsnop  8179  onnseq  8336  fopwdom  9086  fodomfib  9301  intrnfi  9389  ordtypelem5  9497  ordtypelem6  9498  ordtypelem7  9499  ordtypelem8  9500  brwdomn0  9544  wdomtr  9550  fseqenlem2  10031  fin23lem30  10347  isf34lem5  10383  isf34lem7  10384  isf34lem6  10385  fin1a2lem7  10411  ttukeylem6  10519  fodomb  10532  pwxpndom2  10677  hashf1lem1  14522  wrddm  14588  ccatdmss  14649  swrdcl  14715  swrdf1  14721  cats1un  14792  repswswrd  14857  limsupgle  15566  limsupgre  15570  rlim  15584  rlimi  15602  lo1o1  15621  rlimuni  15639  o1co  15675  rlimcn1  15677  ruclem11  16332  1arith  17023  ramval  17104  0ram  17116  mrcuni  17713  homarcl2  18128  prfval  18291  pfxchn  18702  chnind  18713  chnccats1  18717  chnccat  18718  gsumval  18781  gsumval2  18790  mndpsuppss  18874  frmdss2  18973  ghmrn  19357  cntzmhm2  19470  gsumval3  20035  gsumzaddlem  20049  dmdprdd  20129  dprdres  20158  dprdf1  20163  dprd2da  20172  dmdprdsplit2lem  20175  dmdprdsplit2  20176  dmdprdsplit  20177  dprdsplit  20178  dpjidcl  20188  ablfac1eulem  20202  ablfac1eu  20203  ablfaclem2  20216  ablfac2  20219  crngrhmfo  20638  lmhmlsp  21234  rhmpreimaidl  21480  frlmsslsp  22010  f1lindf  22036  mattpostpos  22677  iinopn  23128  lmbrf  23486  cnntri  23497  cnclsi  23498  lmcnp  23530  cnt0  23572  cnt1  23576  cnhaus  23580  cncmp  23618  connima  23651  1stcfb  23671  1stccnp  23689  1stckgenlem  23780  kgencn3  23785  txcnpi  23835  txcnp  23847  prdstps  23856  xkohaus  23880  xkoco2cn  23885  qtopeu  23943  hmeores  23998  fmfnfmlem2  24182  fmfnfmlem4  24184  fmfnfm  24185  lmflf  24232  txflf  24233  cnextfval  24289  cnextcn  24294  clssubg  24336  ghmcnp  24342  qustgplem  24348  tsmsval  24358  ucncn  24511  xmetdmdm  24562  metn0  24587  tmsval  24708  metustid  24781  metustexhalf  24783  metustfbas  24784  isngp2  24824  evth  25188  lmmbrf  25491  iscfil2  25495  caufval  25504  iscau2  25506  caucfil  25512  ovollb2  25718  ovolunlem1a  25725  ovoliunlem1  25731  ovoliun2  25735  ioombl1lem4  25790  uniioombllem1  25810  uniioombllem2  25812  uniioombllem6  25817  mbfconstlem  25856  ismbfcn  25858  mbfmulc2lem  25876  mbfmulc2re  25877  cncombf  25887  mbfaddlem  25889  mbflimsup  25895  i1f0rn  25911  itg1addlem5  25929  itg1climres  25943  mbfmullem2  25953  limcfval  26101  limcdif  26105  ellimc2  26106  ellimc3  26108  limccnp  26120  dvfval  26126  cpnord  26164  cpnres  26166  dvcmul  26173  dvcmulf  26174  dvexp  26182  dvgt0lem1  26231  dvcnvrelem1  26246  itgpowd  26279  plyaddlem1  26440  plymullem1  26441  plycpn  26520  aalioulem3  26567  tayl0  26595  dvntaylp  26604  ulm2  26618  ulmdvlem1  26633  xrlimcnp  27203  dchrelbas2  27471  dchrghm  27490  dchrptlem1  27498  dchrptlem2  27499  iscgrgd  28853  iscgrglt  28854  trgcgrg  28855  tgcgr4  28871  motcgrg  28884  wrdupgr  29528  wrdumgr  29540  grporndm  30977  sspn  31203  fmptcof2  33117  fnpreimac  33130  curry2ima  33168  fpwrelmap  33191  indf1ofs  33299  pmtrcnel  33516  pmtrcnel2  33517  pmtrcnelor  33518  wrdpmtrlast  33520  cycpmcl  33543  cycpmco2f1  33551  cycpmco2rn  33552  cycpmco2lem1  33553  cycpmco2lem2  33554  cycpmco2lem3  33555  cycpmco2lem4  33556  cycpmco2lem5  33557  cycpmco2lem6  33558  cycpmco2lem7  33559  cycpmco2  33560  cyc3co2  33567  cycpmconjv  33569  fxpgaval  33594  rmfsupp2  33664  elrgspnsubrunlem2  33675  rndrhmcl  33724  elrspunidl  33843  rhmimaidl  33847  1arithidomlem2  33933  1arithidom  33934  evls1dm  33958  selvascl  34014  evlextv  34039  esplymhp  34065  esplysply  34068  esplyfval1  34070  ply1degltdimlem  34119  fldextrspunlsp  34171  irngnzply1lem  34187  irngnzply1  34188  zarcmplem  34378  rhmpreimacnlem  34381  esumpcvgval  34575  ofcfval4  34602  measdivcst  34722  oms0  34795  omsmon  34796  omssubaddlem  34797  omssubadd  34798  carsgval  34801  omsmeas  34821  sitgclg  34840  eulerpartlemgu  34875  sseqfv2  34892  rrvdm  34944  ftc2re  35093  cvmliftmolem1  35847  cvmliftlem3  35853  cvmliftlem10  35860  cvmliftlem13  35862  cvmlift2lem9  35877  cvmlift3lem6  35890  cvmlift3lem7  35891  mclsax  36135  mclsppslem  36149  mclspps  36150  fwddifval  36729  fwddifnval  36730  weiunfrlem  37070  bj-finsumval0  38024  curunc  38343  itg2addnclem2  38408  ftc1anclem5  38433  ftc1anclem6  38434  ftc1anclem8  38436  sdclem2  38479  isbnd3  38521  ssbnd  38525  bnd2lem  38528  ismtyval  38537  grpokerinj  38630  rngosn3  38661  rngodm1dm2  38669  divrngcl  38694  isdrngo2  38695  sticksstones1  42999  aks5lem2  43040  evlselvlem  43421  mapfzcons2  43551  fnwe2lem2  43879  lmhmfgima  43912  wnefimgd  44988  binomcxplemnotnn0  45167  cncmpmax  45853  mullimcf  46440  limsuppnfdlem  46516  limsupvaluz  46523  climxrrelem  46564  climxrre  46565  liminfvalxr  46598  liminflimsupxrre  46632  xlimmnfvlem2  46648  xlimpnfvlem2  46652  xlimliminflimsup  46677  cncfuni  46701  cncficcgt0  46703  cncfioobd  46712  dvsinax  46728  itgperiod  46796  fvvolioof  46804  fvvolicof  46806  stoweidlem29  46844  fourierdlem20  46942  fourierdlem48  46969  fourierdlem49  46970  fourierdlem53  46974  fourierdlem63  46984  fourierdlem68  46989  fourierdlem82  47003  fourierdlem113  47034  sge0sn  47194  sge0tsms  47195  sge0cl  47196  sge0isum  47242  ismeannd  47282  hoicvr  47363  dmovn  47419  hspmbl  47444  ovolval4lem1  47464  ovnovollem1  47471  ovnovollem2  47472  issmfd  47550  issmfdf  47552  cnfsmf  47555  issmfled  47572  issmfgtd  47576  smfsuplem1  47626  smfdivdmmbl2  47656  tmachlem-agreesn  47762  fcores  47942  f1cof1blem  47949  f1cof1b  47952  funfocofob  47953  rmsuppss  49287  itcovalendof  49586  ffvbr  49771  lmdran  50584  cmdlan  50585