Theorem fdmd 6673

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5625  ⟶wf 6489

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 6496  df-f 6497

This theorem is referenced by:  fssdmd  6681  fssdm  6682  foima  6752  focnvimacdmdm  6759  resdif  6796  fssrescdmd  7074  fmptco  7077  funfvima2d  7181  focdmex  7903  suppsnop  8123  onnseq  8279  fopwdom  9018  fodomfib  9234  fodomfibOLD  9236  intrnfi  9324  ordtypelem5  9432  ordtypelem6  9433  ordtypelem7  9434  ordtypelem8  9435  brwdomn0  9479  wdomtr  9485  fseqenlem2  9940  fin23lem30  10257  isf34lem5  10293  isf34lem7  10294  isf34lem6  10295  fin1a2lem7  10321  ttukeylem6  10429  fodomb  10441  pwxpndom2  10581  hashf1lem1  14383  wrddm  14449  ccatdmss  14510  swrdcl  14574  cats1un  14649  repswswrd  14712  limsupgle  15405  limsupgre  15409  rlim  15423  rlimi  15441  lo1o1  15460  rlimuni  15478  o1co  15514  rlimcn1  15516  ruclem11  16170  1arith  16860  ramval  16941  0ram  16953  mrcuni  17549  homarcl2  17964  prfval  18127  pfxchn  18538  chnind  18549  chnccats1  18553  chnccat  18554  gsumval  18607  gsumval2  18616  mndpsuppss  18695  frmdss2  18793  ghmrn  19163  cntzmhm2  19276  gsumval3  19841  gsumzaddlem  19855  dmdprdd  19935  dprdres  19964  dprdf1  19969  dprd2da  19978  dmdprdsplit2lem  19981  dmdprdsplit2  19982  dmdprdsplit  19983  dprdsplit  19984  dpjidcl  19994  ablfac1eulem  20008  ablfac1eu  20009  ablfaclem2  20022  ablfac2  20025  lmhmlsp  21006  rhmpreimaidl  21237  frlmsslsp  21756  f1lindf  21782  mattpostpos  22403  iinopn  22851  lmbrf  23209  cnntri  23220  cnclsi  23221  lmcnp  23253  cnt0  23295  cnt1  23299  cnhaus  23303  cncmp  23341  connima  23374  1stcfb  23394  1stccnp  23411  1stckgenlem  23502  kgencn3  23507  txcnpi  23557  txcnp  23569  prdstps  23578  xkohaus  23602  xkoco2cn  23607  qtopeu  23665  hmeores  23720  fmfnfmlem2  23904  fmfnfmlem4  23906  fmfnfm  23907  lmflf  23954  txflf  23955  cnextfval  24011  cnextcn  24016  clssubg  24058  ghmcnp  24064  qustgplem  24070  tsmsval  24080  ucncn  24233  xmetdmdm  24284  metn0  24309  tmsval  24430  metustid  24503  metustexhalf  24505  metustfbas  24506  isngp2  24546  evth  24919  lmmbrf  25223  iscfil2  25227  caufval  25236  iscau2  25238  caucfil  25244  ovollb2  25451  ovolunlem1a  25458  ovoliunlem1  25464  ovoliun2  25468  ioombl1lem4  25523  uniioombllem1  25543  uniioombllem2  25545  uniioombllem6  25550  mbfconstlem  25589  ismbfcn  25591  mbfmulc2lem  25609  mbfmulc2re  25610  cncombf  25620  mbfaddlem  25622  mbflimsup  25628  i1f0rn  25644  itg1addlem5  25662  itg1climres  25676  mbfmullem2  25686  limcfval  25834  limcdif  25838  ellimc2  25839  ellimc3  25841  limccnp  25853  dvfval  25859  cpnord  25898  cpnres  25900  dvcmul  25908  dvcmulf  25909  dvexp  25918  dvgt0lem1  25968  dvcnvrelem1  25983  itgpowd  26018  plyaddlem1  26179  plymullem1  26180  plycpn  26258  aalioulem3  26303  tayl0  26330  dvntaylp  26340  ulm2  26355  ulmdvlem1  26370  xrlimcnp  26939  dchrelbas2  27209  dchrghm  27228  dchrptlem1  27236  dchrptlem2  27237  iscgrgd  28590  iscgrglt  28591  trgcgrg  28592  tgcgr4  28608  motcgrg  28621  wrdupgr  29163  wrdumgr  29175  grporndm  30590  sspn  30816  fmptcof2  32739  fnpreimac  32752  curry2ima  32791  fpwrelmap  32815  indf1ofs  32951  swrdf1  33041  pmtrcnel  33175  pmtrcnel2  33176  pmtrcnelor  33177  wrdpmtrlast  33179  cycpmcl  33202  cycpmco2f1  33210  cycpmco2rn  33211  cycpmco2lem1  33212  cycpmco2lem2  33213  cycpmco2lem3  33214  cycpmco2lem4  33215  cycpmco2lem5  33216  cycpmco2lem6  33217  cycpmco2lem7  33218  cycpmco2  33219  cyc3co2  33226  cycpmconjv  33228  fxpgaval  33253  rmfsupp2  33324  elrgspnsubrunlem2  33334  rndrhmcl  33382  elrspunidl  33513  rhmimaidl  33517  1arithidomlem2  33621  1arithidom  33622  evls1dm  33646  evlextv  33711  esplymhp  33737  esplysply  33740  esplyfval1  33742  ply1degltdimlem  33792  fldextrspunlsp  33844  irngnzply1lem  33860  irngnzply1  33861  zarcmplem  34051  rhmpreimacnlem  34054  esumpcvgval  34248  ofcfval4  34275  measdivcst  34394  oms0  34467  omsmon  34468  omssubaddlem  34469  omssubadd  34470  carsgval  34473  omsmeas  34493  sitgclg  34512  eulerpartlemgu  34547  sseqfv2  34564  rrvdm  34616  ftc2re  34768  cvmliftmolem1  35488  cvmliftlem3  35494  cvmliftlem10  35501  cvmliftlem13  35503  cvmlift2lem9  35518  cvmlift3lem6  35531  cvmlift3lem7  35532  mclsax  35776  mclsppslem  35790  mclspps  35791  fwddifval  36369  fwddifnval  36370  weiunfrlem  36671  bj-finsumval0  37503  curunc  37816  itg2addnclem2  37886  ftc1anclem5  37911  ftc1anclem6  37912  ftc1anclem8  37914  sdclem2  37956  isbnd3  37998  ssbnd  38002  bnd2lem  38005  ismtyval  38014  grpokerinj  38107  rngosn3  38138  rngodm1dm2  38146  divrngcl  38171  isdrngo2  38172  sticksstones1  42479  aks5lem2  42520  evlselvlem  42907  mapfzcons2  43039  fnwe2lem2  43371  lmhmfgima  43404  wnefimgd  44480  binomcxplemnotnn0  44675  cncmpmax  45355  mullimcf  45946  limsuppnfdlem  46022  limsupvaluz  46029  climxrrelem  46070  climxrre  46071  liminfvalxr  46104  liminflimsupxrre  46138  xlimmnfvlem2  46154  xlimpnfvlem2  46158  xlimliminflimsup  46183  cncfuni  46207  cncficcgt0  46209  cncfioobd  46218  dvsinax  46234  itgperiod  46302  fvvolioof  46310  fvvolicof  46312  stoweidlem29  46350  fourierdlem20  46448  fourierdlem53  46480  fourierdlem63  46490  fourierdlem68  46495  fourierdlem82  46509  sge0sn  46700  sge0tsms  46701  sge0cl  46702  sge0isum  46748  ismeannd  46788  hoicvr  46869  dmovn  46925  hspmbl  46950  ovolval4lem1  46970  ovnovollem1  46977  ovnovollem2  46978  issmfd  47056  issmfdf  47058  cnfsmf  47061  issmfled  47078  issmfgtd  47082  smfsuplem1  47132  smfdivdmmbl2  47162  fcores  47390  f1cof1blem  47397  f1cof1b  47400  funfocofob  47401  rmsuppss  48693  itcovalendof  48992  ffvbr  49178  lmdran  49993  cmdlan  49994