Theorem fdmd 6667

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

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5619  ⟶wf 6483

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 6490  df-f 6491

This theorem is referenced by:  fssdmd  6675  fssdm  6676  foima  6746  focnvimacdmdm  6753  resdif  6790  fssrescdmd  7065  fmptco  7068  funfvima2d  7172  focdmex  7894  suppsnop  8114  onnseq  8270  fopwdom  9004  fodomfib  9219  fodomfibOLD  9221  intrnfi  9306  ordtypelem5  9414  ordtypelem6  9415  ordtypelem7  9416  ordtypelem8  9417  brwdomn0  9461  wdomtr  9467  fseqenlem2  9922  fin23lem30  10239  isf34lem5  10275  isf34lem7  10276  isf34lem6  10277  fin1a2lem7  10303  ttukeylem6  10411  fodomb  10423  pwxpndom2  10562  hashf1lem1  14368  wrddm  14434  ccatdmss  14495  swrdcl  14559  cats1un  14634  repswswrd  14697  limsupgle  15390  limsupgre  15394  rlim  15408  rlimi  15426  lo1o1  15445  rlimuni  15463  o1co  15499  rlimcn1  15501  ruclem11  16155  1arith  16845  ramval  16926  0ram  16938  mrcuni  17533  homarcl2  17948  prfval  18111  pfxchn  18522  chnind  18533  chnccats1  18537  chnccat  18538  gsumval  18591  gsumval2  18600  mndpsuppss  18679  frmdss2  18777  ghmrn  19147  cntzmhm2  19260  gsumval3  19825  gsumzaddlem  19839  dmdprdd  19919  dprdres  19948  dprdf1  19953  dprd2da  19962  dmdprdsplit2lem  19965  dmdprdsplit2  19966  dmdprdsplit  19967  dprdsplit  19968  dpjidcl  19978  ablfac1eulem  19992  ablfac1eu  19993  ablfaclem2  20006  ablfac2  20009  lmhmlsp  20989  rhmpreimaidl  21220  frlmsslsp  21739  f1lindf  21765  mattpostpos  22375  iinopn  22823  lmbrf  23181  cnntri  23192  cnclsi  23193  lmcnp  23225  cnt0  23267  cnt1  23271  cnhaus  23275  cncmp  23313  connima  23346  1stcfb  23366  1stccnp  23383  1stckgenlem  23474  kgencn3  23479  txcnpi  23529  txcnp  23541  prdstps  23550  xkohaus  23574  xkoco2cn  23579  qtopeu  23637  hmeores  23692  fmfnfmlem2  23876  fmfnfmlem4  23878  fmfnfm  23879  lmflf  23926  txflf  23927  cnextfval  23983  cnextcn  23988  clssubg  24030  ghmcnp  24036  qustgplem  24042  tsmsval  24052  ucncn  24205  xmetdmdm  24256  metn0  24281  tmsval  24402  metustid  24475  metustexhalf  24477  metustfbas  24478  isngp2  24518  evth  24891  lmmbrf  25195  iscfil2  25199  caufval  25208  iscau2  25210  caucfil  25216  ovollb2  25423  ovolunlem1a  25430  ovoliunlem1  25436  ovoliun2  25440  ioombl1lem4  25495  uniioombllem1  25515  uniioombllem2  25517  uniioombllem6  25522  mbfconstlem  25561  ismbfcn  25563  mbfmulc2lem  25581  mbfmulc2re  25582  cncombf  25592  mbfaddlem  25594  mbflimsup  25600  i1f0rn  25616  itg1addlem5  25634  itg1climres  25648  mbfmullem2  25658  limcfval  25806  limcdif  25810  ellimc2  25811  ellimc3  25813  limccnp  25825  dvfval  25831  cpnord  25870  cpnres  25872  dvcmul  25880  dvcmulf  25881  dvexp  25890  dvgt0lem1  25940  dvcnvrelem1  25955  itgpowd  25990  plyaddlem1  26151  plymullem1  26152  plycpn  26230  aalioulem3  26275  tayl0  26302  dvntaylp  26312  ulm2  26327  ulmdvlem1  26342  xrlimcnp  26911  dchrelbas2  27181  dchrghm  27200  dchrptlem1  27208  dchrptlem2  27209  iscgrgd  28497  iscgrglt  28498  trgcgrg  28499  tgcgr4  28515  motcgrg  28528  wrdupgr  29070  wrdumgr  29082  grporndm  30497  sspn  30723  fmptcof2  32646  fnpreimac  32660  curry2ima  32697  fpwrelmap  32723  indf1ofs  32854  swrdf1  32944  pmtrcnel  33065  pmtrcnel2  33066  pmtrcnelor  33067  wrdpmtrlast  33069  cycpmcl  33092  cycpmco2f1  33100  cycpmco2rn  33101  cycpmco2lem1  33102  cycpmco2lem2  33103  cycpmco2lem3  33104  cycpmco2lem4  33105  cycpmco2lem5  33106  cycpmco2lem6  33107  cycpmco2lem7  33108  cycpmco2  33109  cyc3co2  33116  cycpmconjv  33118  fxpgaval  33143  rmfsupp2  33212  elrgspnsubrunlem2  33222  rndrhmcl  33269  elrspunidl  33400  rhmimaidl  33404  1arithidomlem2  33508  1arithidom  33509  evls1dm  33531  esplymhp  33596  esplysply  33599  ply1degltdimlem  33642  fldextrspunlsp  33694  irngnzply1lem  33710  irngnzply1  33711  zarcmplem  33901  rhmpreimacnlem  33904  esumpcvgval  34098  ofcfval4  34125  measdivcst  34244  oms0  34317  omsmon  34318  omssubaddlem  34319  omssubadd  34320  carsgval  34323  omsmeas  34343  sitgclg  34362  eulerpartlemgu  34397  sseqfv2  34414  rrvdm  34466  ftc2re  34618  cvmliftmolem1  35332  cvmliftlem3  35338  cvmliftlem10  35345  cvmliftlem13  35347  cvmlift2lem9  35362  cvmlift3lem6  35375  cvmlift3lem7  35376  mclsax  35620  mclsppslem  35634  mclspps  35635  fwddifval  36213  fwddifnval  36214  weiunfrlem  36515  bj-finsumval0  37336  curunc  37648  itg2addnclem2  37718  ftc1anclem5  37743  ftc1anclem6  37744  ftc1anclem8  37746  sdclem2  37788  isbnd3  37830  ssbnd  37834  bnd2lem  37837  ismtyval  37846  grpokerinj  37939  rngosn3  37970  rngodm1dm2  37978  divrngcl  38003  isdrngo2  38004  sticksstones1  42245  aks5lem2  42286  evlselvlem  42685  mapfzcons2  42817  fnwe2lem2  43149  lmhmfgima  43182  wnefimgd  44259  binomcxplemnotnn0  44454  cncmpmax  45134  mullimcf  45728  limsuppnfdlem  45804  limsupvaluz  45811  climxrrelem  45852  climxrre  45853  liminfvalxr  45886  liminflimsupxrre  45920  xlimmnfvlem2  45936  xlimpnfvlem2  45940  xlimliminflimsup  45965  cncfuni  45989  cncficcgt0  45991  cncfioobd  46000  dvsinax  46016  itgperiod  46084  fvvolioof  46092  fvvolicof  46094  stoweidlem29  46132  fourierdlem20  46230  fourierdlem53  46262  fourierdlem63  46272  fourierdlem68  46277  fourierdlem82  46291  sge0sn  46482  sge0tsms  46483  sge0cl  46484  sge0isum  46530  ismeannd  46570  hoicvr  46651  dmovn  46707  hspmbl  46732  ovolval4lem1  46752  ovnovollem1  46759  ovnovollem2  46760  issmfd  46838  issmfdf  46840  cnfsmf  46843  issmfled  46860  issmfgtd  46864  smfsuplem1  46914  smfdivdmmbl2  46944  fcores  47172  f1cof1blem  47179  f1cof1b  47182  funfocofob  47183  rmsuppss  48475  itcovalendof  48775  ffvbr  48961  lmdran  49777  cmdlan  49778