Theorem fdmd 6523

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

Syntax hints:   → wi 4   = wceq 1537  dom cdm 5555  ⟶wf 6351

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 209  df-an 399  df-fn 6358  df-f 6359

This theorem is referenced by:  fssdmd  6529  fssdm  6530  foima  6595  resdif  6635  fmptco  6891  funfvima2d  6994  fornex  7657  suppsnop  7844  onnseq  7981  fopwdom  8625  fodomfib  8798  intrnfi  8880  ordtypelem5  8986  ordtypelem6  8987  ordtypelem7  8988  ordtypelem8  8989  brwdomn0  9033  wdomtr  9039  fseqenlem2  9451  fin23lem30  9764  isf34lem5  9800  isf34lem7  9801  isf34lem6  9802  fin1a2lem7  9828  ttukeylem6  9936  fodomb  9948  pwxpndom2  10087  hashf1lem1  13814  wrddm  13869  swrdcl  14007  cats1un  14083  repswswrd  14146  limsupgle  14834  limsupgre  14838  rlim  14852  rlimi  14870  lo1o1  14889  rlimuni  14907  o1co  14943  rlimcn1  14945  ruclem11  15593  1arith  16263  ramval  16344  0ram  16356  mrcuni  16892  homarcl2  17295  prfval  17449  gsumval  17887  gsumval2  17896  frmdss2  18028  ghmrn  18371  cntzmhm2  18470  gsumval3  19027  gsumzaddlem  19041  dmdprdd  19121  dprdres  19150  dprdf1  19155  dprd2da  19164  dmdprdsplit2lem  19167  dmdprdsplit2  19168  dmdprdsplit  19169  dprdsplit  19170  dpjidcl  19180  ablfac1eulem  19194  ablfac1eu  19195  ablfaclem2  19208  ablfac2  19211  lmhmlsp  19821  frlmsslsp  20940  f1lindf  20966  mattpostpos  21063  iinopn  21510  lmbrf  21868  cnntri  21879  cnclsi  21880  lmcnp  21912  cnt0  21954  cnt1  21958  cnhaus  21962  cncmp  22000  connima  22033  1stcfb  22053  1stccnp  22070  1stckgenlem  22161  kgencn3  22166  txcnpi  22216  txcnp  22228  prdstps  22237  xkohaus  22261  xkoco2cn  22266  qtopeu  22324  hmeores  22379  fmfnfmlem2  22563  fmfnfmlem4  22565  fmfnfm  22566  lmflf  22613  txflf  22614  cnextfval  22670  cnextcn  22675  clssubg  22717  ghmcnp  22723  qustgplem  22729  tsmsval  22739  ucncn  22894  xmetdmdm  22945  metn0  22970  tmsval  23091  metustid  23164  metustexhalf  23166  metustfbas  23167  isngp2  23206  evth  23563  lmmbrf  23865  iscfil2  23869  caufval  23878  iscau2  23880  caucfil  23886  ovollb2  24090  ovolunlem1a  24097  ovoliunlem1  24103  ovoliun2  24107  ioombl1lem4  24162  uniioombllem1  24182  uniioombllem2  24184  uniioombllem6  24189  mbfconstlem  24228  ismbfcn  24230  mbfmulc2lem  24248  mbfmulc2re  24249  cncombf  24259  mbfaddlem  24261  mbflimsup  24267  i1f0rn  24283  itg1addlem5  24301  itg1climres  24315  mbfmullem2  24325  limcfval  24470  limcdif  24474  ellimc2  24475  ellimc3  24477  limccnp  24489  dvfval  24495  cpnord  24532  cpnres  24534  dvcmul  24541  dvcmulf  24542  dvexp  24550  dvgt0lem1  24599  dvcnvrelem1  24614  plyaddlem1  24803  plymullem1  24804  plycpn  24878  aalioulem3  24923  tayl0  24950  dvntaylp  24959  ulm2  24973  ulmdvlem1  24988  xrlimcnp  25546  dchrelbas2  25813  dchrghm  25832  dchrptlem1  25840  dchrptlem2  25841  iscgrgd  26299  iscgrglt  26300  trgcgrg  26301  tgcgr4  26317  motcgrg  26330  wrdupgr  26870  wrdumgr  26882  grporndm  28287  sspn  28513  fmptcof2  30402  fnpreimac  30416  curry2ima  30444  fpwrelmap  30469  swrdf1  30630  pmtrcnel  30733  pmtrcnel2  30734  pmtrcnelor  30735  cycpmcl  30758  cycpmco2f1  30766  cycpmco2rn  30767  cycpmco2lem1  30768  cycpmco2lem2  30769  cycpmco2lem3  30770  cycpmco2lem4  30771  cycpmco2lem5  30772  cycpmco2lem6  30773  cycpmco2lem7  30774  cycpmco2  30775  cyc3co2  30782  cycpmconjv  30784  rmfsupp2  30866  indf1ofs  31285  esumpcvgval  31337  ofcfval4  31364  measdivcst  31483  oms0  31555  omsmon  31556  omssubaddlem  31557  omssubadd  31558  carsgval  31561  omsmeas  31581  sitgclg  31600  eulerpartlemgu  31635  sseqfv2  31652  rrvdm  31704  ftc2re  31869  cvmliftmolem1  32528  cvmliftlem3  32534  cvmliftlem10  32541  cvmliftlem13  32543  cvmlift2lem9  32558  cvmlift3lem6  32571  cvmlift3lem7  32572  mclsax  32816  mclsppslem  32830  mclspps  32831  fwddifval  33623  fwddifnval  33624  bj-finsumval0  34570  curunc  34889  itg2addnclem2  34959  ftc1anclem5  34986  ftc1anclem6  34987  ftc1anclem8  34989  sdclem2  35032  isbnd3  35077  ssbnd  35081  bnd2lem  35084  ismtyval  35093  grpokerinj  35186  rngosn3  35217  rngodm1dm2  35225  divrngcl  35250  isdrngo2  35251  mapfzcons2  39336  fnwe2lem2  39671  lmhmfgima  39704  itgpowd  39841  wnefimgd  40532  binomcxplemnotnn0  40708  cncmpmax  41309  mullimcf  41924  limsuppnfdlem  42002  limsupvaluz  42009  climxrrelem  42050  climxrre  42051  liminfvalxr  42084  liminflimsupxrre  42118  xlimmnfvlem2  42134  xlimpnfvlem2  42138  xlimliminflimsup  42163  cncfuni  42189  cncficcgt0  42191  cncfioobd  42200  dvsinax  42217  itgperiod  42286  fvvolioof  42294  fvvolicof  42296  stoweidlem29  42334  fourierdlem20  42432  fourierdlem53  42464  fourierdlem63  42474  fourierdlem68  42479  fourierdlem82  42493  sge0sn  42681  sge0tsms  42682  sge0cl  42683  sge0isum  42729  ismeannd  42769  hoicvr  42850  dmovn  42906  hspmbl  42931  ovolval4lem1  42951  ovnovollem1  42958  ovnovollem2  42959  issmfd  43032  issmfdf  43034  cnfsmf  43037  issmfled  43054  smfmbfcex  43056  issmfgtd  43057  smfsuplem1  43105  rmsuppss  44438  mndpsuppss  44439