Theorem fdmd 6716

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

Syntax hints:   → wi 4   = wceq 1568  dom cdm 5661  ⟶wf 6532

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 210  df-an 401  df-fn 6539  df-f 6540

This theorem is referenced by:  fssdmd  6724  fssdm  6725  foima  6797  focnvimacdmdm  6804  resdif  6842  fssrescdmd  7122  fmptco  7125  funfvima2d  7230  focdmex  7952  suppsnop  8173  onnseq  8330  fopwdom  9072  fodomfib  9287  intrnfi  9375  ordtypelem5  9483  ordtypelem6  9484  ordtypelem7  9485  ordtypelem8  9486  brwdomn0  9530  wdomtr  9536  fseqenlem2  10008  fin23lem30  10325  isf34lem5  10361  isf34lem7  10362  isf34lem6  10363  fin1a2lem7  10389  ttukeylem6  10497  fodomb  10509  pwxpndom2  10649  hashf1lem1  14491  wrddm  14557  ccatdmss  14618  swrdcl  14682  cats1un  14757  repswswrd  14820  limsupgle  15527  limsupgre  15531  rlim  15545  rlimi  15563  lo1o1  15582  rlimuni  15600  o1co  15636  rlimcn1  15638  ruclem11  16295  1arith  16986  ramval  17067  0ram  17079  mrcuni  17676  homarcl2  18091  prfval  18254  pfxchn  18665  chnind  18676  chnccats1  18680  chnccat  18681  gsumval  18734  gsumval2  18743  mndpsuppss  18822  frmdss2  18921  ghmrn  19298  cntzmhm2  19411  gsumval3  19976  gsumzaddlem  19990  dmdprdd  20070  dprdres  20099  dprdf1  20104  dprd2da  20113  dmdprdsplit2lem  20116  dmdprdsplit2  20117  dmdprdsplit  20118  dprdsplit  20119  dpjidcl  20129  ablfac1eulem  20143  ablfac1eu  20144  ablfaclem2  20157  ablfac2  20160  lmhmlsp  21149  rhmpreimaidl  21395  frlmsslsp  21925  f1lindf  21951  mattpostpos  22590  iinopn  23038  lmbrf  23396  cnntri  23407  cnclsi  23408  lmcnp  23440  cnt0  23482  cnt1  23486  cnhaus  23490  cncmp  23528  connima  23561  1stcfb  23581  1stccnp  23598  1stckgenlem  23689  kgencn3  23694  txcnpi  23744  txcnp  23756  prdstps  23765  xkohaus  23789  xkoco2cn  23794  qtopeu  23852  hmeores  23907  fmfnfmlem2  24091  fmfnfmlem4  24093  fmfnfm  24094  lmflf  24141  txflf  24142  cnextfval  24198  cnextcn  24203  clssubg  24245  ghmcnp  24251  qustgplem  24257  tsmsval  24267  ucncn  24420  xmetdmdm  24471  metn0  24496  tmsval  24617  metustid  24690  metustexhalf  24692  metustfbas  24693  isngp2  24733  evth  25097  lmmbrf  25400  iscfil2  25404  caufval  25413  iscau2  25415  caucfil  25421  ovollb2  25627  ovolunlem1a  25634  ovoliunlem1  25640  ovoliun2  25644  ioombl1lem4  25699  uniioombllem1  25719  uniioombllem2  25721  uniioombllem6  25726  mbfconstlem  25765  ismbfcn  25767  mbfmulc2lem  25785  mbfmulc2re  25786  cncombf  25796  mbfaddlem  25798  mbflimsup  25804  i1f0rn  25820  itg1addlem5  25838  itg1climres  25852  mbfmullem2  25862  limcfval  26010  limcdif  26014  ellimc2  26015  ellimc3  26017  limccnp  26029  dvfval  26035  cpnord  26073  cpnres  26075  dvcmul  26082  dvcmulf  26083  dvexp  26091  dvgt0lem1  26140  dvcnvrelem1  26155  itgpowd  26188  plyaddlem1  26349  plymullem1  26350  plycpn  26429  aalioulem3  26474  tayl0  26501  dvntaylp  26510  ulm2  26524  ulmdvlem1  26539  xrlimcnp  27109  dchrelbas2  27377  dchrghm  27396  dchrptlem1  27404  dchrptlem2  27405  iscgrgd  28758  iscgrglt  28759  trgcgrg  28760  tgcgr4  28776  motcgrg  28789  wrdupgr  29401  wrdumgr  29413  grporndm  30828  sspn  31054  fmptcof2  32968  fnpreimac  32981  curry2ima  33020  fpwrelmap  33044  indf1ofs  33152  swrdf1  33242  pmtrcnel  33375  pmtrcnel2  33376  pmtrcnelor  33377  wrdpmtrlast  33379  cycpmcl  33402  cycpmco2f1  33410  cycpmco2rn  33411  cycpmco2lem1  33412  cycpmco2lem2  33413  cycpmco2lem3  33414  cycpmco2lem4  33415  cycpmco2lem5  33416  cycpmco2lem6  33417  cycpmco2lem7  33418  cycpmco2  33419  cyc3co2  33426  cycpmconjv  33428  fxpgaval  33453  rmfsupp2  33523  elrgspnsubrunlem2  33534  rndrhmcl  33583  elrspunidl  33702  rhmimaidl  33706  1arithidomlem2  33792  1arithidom  33793  evls1dm  33817  selvascl  33873  evlextv  33898  esplymhp  33924  esplysply  33927  esplyfval1  33929  ply1degltdimlem  33978  fldextrspunlsp  34030  irngnzply1lem  34046  irngnzply1  34047  zarcmplem  34237  rhmpreimacnlem  34240  esumpcvgval  34434  ofcfval4  34461  measdivcst  34580  oms0  34653  omsmon  34654  omssubaddlem  34655  omssubadd  34656  carsgval  34659  omsmeas  34679  sitgclg  34698  eulerpartlemgu  34733  sseqfv2  34750  rrvdm  34802  ftc2re  34951  cvmliftmolem1  35727  cvmliftlem3  35733  cvmliftlem10  35740  cvmliftlem13  35742  cvmlift2lem9  35757  cvmlift3lem6  35770  cvmlift3lem7  35771  mclsax  36015  mclsppslem  36029  mclspps  36030  fwddifval  36608  fwddifnval  36609  weiunfrlem  36919  bj-finsumval0  37873  curunc  38197  itg2addnclem2  38267  ftc1anclem5  38292  ftc1anclem6  38293  ftc1anclem8  38295  sdclem2  38337  isbnd3  38379  ssbnd  38383  bnd2lem  38386  ismtyval  38395  grpokerinj  38488  rngosn3  38519  rngodm1dm2  38527  divrngcl  38552  isdrngo2  38553  sticksstones1  42859  aks5lem2  42900  evlselvlem  43268  mapfzcons2  43398  fnwe2lem2  43726  lmhmfgima  43759  wnefimgd  44835  binomcxplemnotnn0  45014  cncmpmax  45700  mullimcf  46287  limsuppnfdlem  46363  limsupvaluz  46370  climxrrelem  46411  climxrre  46412  liminfvalxr  46445  liminflimsupxrre  46479  xlimmnfvlem2  46495  xlimpnfvlem2  46499  xlimliminflimsup  46524  cncfuni  46548  cncficcgt0  46550  cncfioobd  46559  dvsinax  46575  itgperiod  46643  fvvolioof  46651  fvvolicof  46653  stoweidlem29  46691  fourierdlem20  46789  fourierdlem48  46816  fourierdlem49  46817  fourierdlem53  46821  fourierdlem63  46831  fourierdlem68  46836  fourierdlem82  46850  fourierdlem113  46881  sge0sn  47041  sge0tsms  47042  sge0cl  47043  sge0isum  47089  ismeannd  47129  hoicvr  47210  dmovn  47266  hspmbl  47291  ovolval4lem1  47311  ovnovollem1  47318  ovnovollem2  47319  issmfd  47397  issmfdf  47399  cnfsmf  47402  issmfled  47419  issmfgtd  47423  smfsuplem1  47473  smfdivdmmbl2  47503  fcores  47749  f1cof1blem  47756  f1cof1b  47759  funfocofob  47760  rmsuppss  49095  itcovalendof  49394  ffvbr  49579  lmdran  50394  cmdlan  50395