Theorem fdmd 6620

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

Syntax hints:   → wi 4   = wceq 1539  dom cdm 5590  ⟶wf 6433

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 206  df-an 397  df-fn 6440  df-f 6441

This theorem is referenced by:  fssdmd  6628  fssdm  6629  foima  6702  focnvimacdmdm  6709  resdif  6746  fmptco  7010  funfvima2d  7117  fornex  7807  suppsnop  8003  onnseq  8184  fopwdom  8876  fodomfib  9102  intrnfi  9184  ordtypelem5  9290  ordtypelem6  9291  ordtypelem7  9292  ordtypelem8  9293  brwdomn0  9337  wdomtr  9343  fseqenlem2  9790  fin23lem30  10107  isf34lem5  10143  isf34lem7  10144  isf34lem6  10145  fin1a2lem7  10171  ttukeylem6  10279  fodomb  10291  pwxpndom2  10430  hashf1lem1  14177  hashf1lem1OLD  14178  wrddm  14233  swrdcl  14367  cats1un  14443  repswswrd  14506  limsupgle  15195  limsupgre  15199  rlim  15213  rlimi  15231  lo1o1  15250  rlimuni  15268  o1co  15304  rlimcn1  15306  ruclem11  15958  1arith  16637  ramval  16718  0ram  16730  mrcuni  17339  homarcl2  17759  prfval  17925  gsumval  18370  gsumval2  18379  frmdss2  18511  ghmrn  18856  cntzmhm2  18955  gsumval3  19517  gsumzaddlem  19531  dmdprdd  19611  dprdres  19640  dprdf1  19645  dprd2da  19654  dmdprdsplit2lem  19657  dmdprdsplit2  19658  dmdprdsplit  19659  dprdsplit  19660  dpjidcl  19670  ablfac1eulem  19684  ablfac1eu  19685  ablfaclem2  19698  ablfac2  19701  lmhmlsp  20320  frlmsslsp  21012  f1lindf  21038  mattpostpos  21612  iinopn  22060  lmbrf  22420  cnntri  22431  cnclsi  22432  lmcnp  22464  cnt0  22506  cnt1  22510  cnhaus  22514  cncmp  22552  connima  22585  1stcfb  22605  1stccnp  22622  1stckgenlem  22713  kgencn3  22718  txcnpi  22768  txcnp  22780  prdstps  22789  xkohaus  22813  xkoco2cn  22818  qtopeu  22876  hmeores  22931  fmfnfmlem2  23115  fmfnfmlem4  23117  fmfnfm  23118  lmflf  23165  txflf  23166  cnextfval  23222  cnextcn  23227  clssubg  23269  ghmcnp  23275  qustgplem  23281  tsmsval  23291  ucncn  23446  xmetdmdm  23497  metn0  23522  tmsval  23645  metustid  23719  metustexhalf  23721  metustfbas  23722  isngp2  23762  evth  24131  lmmbrf  24435  iscfil2  24439  caufval  24448  iscau2  24450  caucfil  24456  ovollb2  24662  ovolunlem1a  24669  ovoliunlem1  24675  ovoliun2  24679  ioombl1lem4  24734  uniioombllem1  24754  uniioombllem2  24756  uniioombllem6  24761  mbfconstlem  24800  ismbfcn  24802  mbfmulc2lem  24820  mbfmulc2re  24821  cncombf  24831  mbfaddlem  24833  mbflimsup  24839  i1f0rn  24855  itg1addlem5  24874  itg1climres  24888  mbfmullem2  24898  limcfval  25045  limcdif  25049  ellimc2  25050  ellimc3  25052  limccnp  25064  dvfval  25070  cpnord  25108  cpnres  25110  dvcmul  25117  dvcmulf  25118  dvexp  25126  dvgt0lem1  25175  dvcnvrelem1  25190  itgpowd  25223  plyaddlem1  25383  plymullem1  25384  plycpn  25458  aalioulem3  25503  tayl0  25530  dvntaylp  25539  ulm2  25553  ulmdvlem1  25568  xrlimcnp  26127  dchrelbas2  26394  dchrghm  26413  dchrptlem1  26421  dchrptlem2  26422  iscgrgd  26883  iscgrglt  26884  trgcgrg  26885  tgcgr4  26901  motcgrg  26914  wrdupgr  27464  wrdumgr  27476  grporndm  28881  sspn  29107  fmptcof2  31003  fnpreimac  31017  curry2ima  31050  fpwrelmap  31077  swrdf1  31237  pmtrcnel  31367  pmtrcnel2  31368  pmtrcnelor  31369  cycpmcl  31392  cycpmco2f1  31400  cycpmco2rn  31401  cycpmco2lem1  31402  cycpmco2lem2  31403  cycpmco2lem3  31404  cycpmco2lem4  31405  cycpmco2lem5  31406  cycpmco2lem6  31407  cycpmco2lem7  31408  cycpmco2  31409  cyc3co2  31416  cycpmconjv  31418  rmfsupp2  31501  rhmpreimaidl  31612  elrspunidl  31615  rhmimaidl  31618  zarcmplem  31840  rhmpreimacnlem  31843  indf1ofs  32003  esumpcvgval  32055  ofcfval4  32082  measdivcst  32201  oms0  32273  omsmon  32274  omssubaddlem  32275  omssubadd  32276  carsgval  32279  omsmeas  32299  sitgclg  32318  eulerpartlemgu  32353  sseqfv2  32370  rrvdm  32422  ftc2re  32587  cvmliftmolem1  33252  cvmliftlem3  33258  cvmliftlem10  33265  cvmliftlem13  33267  cvmlift2lem9  33282  cvmlift3lem6  33295  cvmlift3lem7  33296  mclsax  33540  mclsppslem  33554  mclspps  33555  fwddifval  34473  fwddifnval  34474  bj-finsumval0  35465  curunc  35768  itg2addnclem2  35838  ftc1anclem5  35863  ftc1anclem6  35864  ftc1anclem8  35866  sdclem2  35909  isbnd3  35951  ssbnd  35955  bnd2lem  35958  ismtyval  35967  grpokerinj  36060  rngosn3  36091  rngodm1dm2  36099  divrngcl  36124  isdrngo2  36125  sticksstones1  40109  mapfzcons2  40548  fnwe2lem2  40883  lmhmfgima  40916  wnefimgd  41779  binomcxplemnotnn0  41981  cncmpmax  42582  mullimcf  43171  limsuppnfdlem  43249  limsupvaluz  43256  climxrrelem  43297  climxrre  43298  liminfvalxr  43331  liminflimsupxrre  43365  xlimmnfvlem2  43381  xlimpnfvlem2  43385  xlimliminflimsup  43410  cncfuni  43434  cncficcgt0  43436  cncfioobd  43445  dvsinax  43461  itgperiod  43529  fvvolioof  43537  fvvolicof  43539  stoweidlem29  43577  fourierdlem20  43675  fourierdlem53  43707  fourierdlem63  43717  fourierdlem68  43722  fourierdlem82  43736  sge0sn  43924  sge0tsms  43925  sge0cl  43926  sge0isum  43972  ismeannd  44012  hoicvr  44093  dmovn  44149  hspmbl  44174  ovolval4lem1  44194  ovnovollem1  44201  ovnovollem2  44202  issmfd  44280  issmfdf  44282  cnfsmf  44285  issmfled  44302  issmfgtd  44306  smfsuplem1  44355  fcores  44572  f1cof1blem  44579  f1cof1b  44580  funfocofob  44581  rmsuppss  45717  mndpsuppss  45718  itcovalendof  46026