Theorem fdmd 6701

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5641  ⟶wf 6510

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 207  df-an 396  df-fn 6517  df-f 6518

This theorem is referenced by:  fssdmd  6709  fssdm  6710  foima  6780  focnvimacdmdm  6787  resdif  6824  fssrescdmd  7101  fmptco  7104  funfvima2d  7209  focdmex  7937  suppsnop  8160  onnseq  8316  fopwdom  9054  fodomfib  9287  fodomfibOLD  9289  intrnfi  9374  ordtypelem5  9482  ordtypelem6  9483  ordtypelem7  9484  ordtypelem8  9485  brwdomn0  9529  wdomtr  9535  fseqenlem2  9985  fin23lem30  10302  isf34lem5  10338  isf34lem7  10339  isf34lem6  10340  fin1a2lem7  10366  ttukeylem6  10474  fodomb  10486  pwxpndom2  10625  hashf1lem1  14427  wrddm  14493  swrdcl  14617  cats1un  14693  repswswrd  14756  limsupgle  15450  limsupgre  15454  rlim  15468  rlimi  15486  lo1o1  15505  rlimuni  15523  o1co  15559  rlimcn1  15561  ruclem11  16215  1arith  16905  ramval  16986  0ram  16998  mrcuni  17589  homarcl2  18004  prfval  18167  gsumval  18611  gsumval2  18620  mndpsuppss  18699  frmdss2  18797  ghmrn  19168  cntzmhm2  19281  gsumval3  19844  gsumzaddlem  19858  dmdprdd  19938  dprdres  19967  dprdf1  19972  dprd2da  19981  dmdprdsplit2lem  19984  dmdprdsplit2  19985  dmdprdsplit  19986  dprdsplit  19987  dpjidcl  19997  ablfac1eulem  20011  ablfac1eu  20012  ablfaclem2  20025  ablfac2  20028  lmhmlsp  20963  rhmpreimaidl  21194  frlmsslsp  21712  f1lindf  21738  mattpostpos  22348  iinopn  22796  lmbrf  23154  cnntri  23165  cnclsi  23166  lmcnp  23198  cnt0  23240  cnt1  23244  cnhaus  23248  cncmp  23286  connima  23319  1stcfb  23339  1stccnp  23356  1stckgenlem  23447  kgencn3  23452  txcnpi  23502  txcnp  23514  prdstps  23523  xkohaus  23547  xkoco2cn  23552  qtopeu  23610  hmeores  23665  fmfnfmlem2  23849  fmfnfmlem4  23851  fmfnfm  23852  lmflf  23899  txflf  23900  cnextfval  23956  cnextcn  23961  clssubg  24003  ghmcnp  24009  qustgplem  24015  tsmsval  24025  ucncn  24179  xmetdmdm  24230  metn0  24255  tmsval  24376  metustid  24449  metustexhalf  24451  metustfbas  24452  isngp2  24492  evth  24865  lmmbrf  25169  iscfil2  25173  caufval  25182  iscau2  25184  caucfil  25190  ovollb2  25397  ovolunlem1a  25404  ovoliunlem1  25410  ovoliun2  25414  ioombl1lem4  25469  uniioombllem1  25489  uniioombllem2  25491  uniioombllem6  25496  mbfconstlem  25535  ismbfcn  25537  mbfmulc2lem  25555  mbfmulc2re  25556  cncombf  25566  mbfaddlem  25568  mbflimsup  25574  i1f0rn  25590  itg1addlem5  25608  itg1climres  25622  mbfmullem2  25632  limcfval  25780  limcdif  25784  ellimc2  25785  ellimc3  25787  limccnp  25799  dvfval  25805  cpnord  25844  cpnres  25846  dvcmul  25854  dvcmulf  25855  dvexp  25864  dvgt0lem1  25914  dvcnvrelem1  25929  itgpowd  25964  plyaddlem1  26125  plymullem1  26126  plycpn  26204  aalioulem3  26249  tayl0  26276  dvntaylp  26286  ulm2  26301  ulmdvlem1  26316  xrlimcnp  26885  dchrelbas2  27155  dchrghm  27174  dchrptlem1  27182  dchrptlem2  27183  iscgrgd  28447  iscgrglt  28448  trgcgrg  28449  tgcgr4  28465  motcgrg  28478  wrdupgr  29019  wrdumgr  29031  grporndm  30446  sspn  30672  fmptcof2  32588  fnpreimac  32602  curry2ima  32639  fpwrelmap  32663  indf1ofs  32796  ccatdmss  32878  swrdf1  32885  pfxchn  32942  chnind  32944  chnccats1  32948  pmtrcnel  33053  pmtrcnel2  33054  pmtrcnelor  33055  wrdpmtrlast  33057  cycpmcl  33080  cycpmco2f1  33088  cycpmco2rn  33089  cycpmco2lem1  33090  cycpmco2lem2  33091  cycpmco2lem3  33092  cycpmco2lem4  33093  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2lem7  33096  cycpmco2  33097  cyc3co2  33104  cycpmconjv  33106  fxpgaval  33131  rmfsupp2  33196  elrgspnsubrunlem2  33206  rndrhmcl  33253  elrspunidl  33406  rhmimaidl  33410  1arithidomlem2  33514  1arithidom  33515  evls1dm  33537  ply1degltdimlem  33625  fldextrspunlsp  33676  irngnzply1lem  33692  irngnzply1  33693  zarcmplem  33878  rhmpreimacnlem  33881  esumpcvgval  34075  ofcfval4  34102  measdivcst  34221  oms0  34295  omsmon  34296  omssubaddlem  34297  omssubadd  34298  carsgval  34301  omsmeas  34321  sitgclg  34340  eulerpartlemgu  34375  sseqfv2  34392  rrvdm  34444  ftc2re  34596  cvmliftmolem1  35275  cvmliftlem3  35281  cvmliftlem10  35288  cvmliftlem13  35290  cvmlift2lem9  35305  cvmlift3lem6  35318  cvmlift3lem7  35319  mclsax  35563  mclsppslem  35577  mclspps  35578  fwddifval  36157  fwddifnval  36158  weiunfrlem  36459  bj-finsumval0  37280  curunc  37603  itg2addnclem2  37673  ftc1anclem5  37698  ftc1anclem6  37699  ftc1anclem8  37701  sdclem2  37743  isbnd3  37785  ssbnd  37789  bnd2lem  37792  ismtyval  37801  grpokerinj  37894  rngosn3  37925  rngodm1dm2  37933  divrngcl  37958  isdrngo2  37959  sticksstones1  42141  aks5lem2  42182  evlselvlem  42581  mapfzcons2  42714  fnwe2lem2  43047  lmhmfgima  43080  wnefimgd  44157  binomcxplemnotnn0  44352  cncmpmax  45033  mullimcf  45628  limsuppnfdlem  45706  limsupvaluz  45713  climxrrelem  45754  climxrre  45755  liminfvalxr  45788  liminflimsupxrre  45822  xlimmnfvlem2  45838  xlimpnfvlem2  45842  xlimliminflimsup  45867  cncfuni  45891  cncficcgt0  45893  cncfioobd  45902  dvsinax  45918  itgperiod  45986  fvvolioof  45994  fvvolicof  45996  stoweidlem29  46034  fourierdlem20  46132  fourierdlem53  46164  fourierdlem63  46174  fourierdlem68  46179  fourierdlem82  46193  sge0sn  46384  sge0tsms  46385  sge0cl  46386  sge0isum  46432  ismeannd  46472  hoicvr  46553  dmovn  46609  hspmbl  46634  ovolval4lem1  46654  ovnovollem1  46661  ovnovollem2  46662  issmfd  46740  issmfdf  46742  cnfsmf  46745  issmfled  46762  issmfgtd  46766  smfsuplem1  46816  smfdivdmmbl2  46846  fcores  47072  f1cof1blem  47079  f1cof1b  47082  funfocofob  47083  rmsuppss  48362  itcovalendof  48662  ffvbr  48848  lmdran  49664  cmdlan  49665