Theorem fdmd 6670

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5622  ⟶wf 6486

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 6493  df-f 6494

This theorem is referenced by:  fssdmd  6678  fssdm  6679  foima  6749  focnvimacdmdm  6756  resdif  6793  fssrescdmd  7071  fmptco  7074  funfvima2d  7178  focdmex  7900  suppsnop  8119  onnseq  8275  fopwdom  9014  fodomfib  9230  fodomfibOLD  9232  intrnfi  9320  ordtypelem5  9428  ordtypelem6  9429  ordtypelem7  9430  ordtypelem8  9431  brwdomn0  9475  wdomtr  9481  fseqenlem2  9936  fin23lem30  10253  isf34lem5  10289  isf34lem7  10290  isf34lem6  10291  fin1a2lem7  10317  ttukeylem6  10425  fodomb  10437  pwxpndom2  10577  hashf1lem1  14379  wrddm  14445  ccatdmss  14506  swrdcl  14570  cats1un  14645  repswswrd  14708  limsupgle  15401  limsupgre  15405  rlim  15419  rlimi  15437  lo1o1  15456  rlimuni  15474  o1co  15510  rlimcn1  15512  ruclem11  16166  1arith  16856  ramval  16937  0ram  16949  mrcuni  17545  homarcl2  17960  prfval  18123  pfxchn  18534  chnind  18545  chnccats1  18549  chnccat  18550  gsumval  18603  gsumval2  18612  mndpsuppss  18691  frmdss2  18789  ghmrn  19162  cntzmhm2  19275  gsumval3  19840  gsumzaddlem  19854  dmdprdd  19934  dprdres  19963  dprdf1  19968  dprd2da  19977  dmdprdsplit2lem  19980  dmdprdsplit2  19981  dmdprdsplit  19982  dprdsplit  19983  dpjidcl  19993  ablfac1eulem  20007  ablfac1eu  20008  ablfaclem2  20021  ablfac2  20024  lmhmlsp  21003  rhmpreimaidl  21234  frlmsslsp  21753  f1lindf  21779  mattpostpos  22397  iinopn  22845  lmbrf  23203  cnntri  23214  cnclsi  23215  lmcnp  23247  cnt0  23289  cnt1  23293  cnhaus  23297  cncmp  23335  connima  23368  1stcfb  23388  1stccnp  23405  1stckgenlem  23496  kgencn3  23501  txcnpi  23551  txcnp  23563  prdstps  23572  xkohaus  23596  xkoco2cn  23601  qtopeu  23659  hmeores  23714  fmfnfmlem2  23898  fmfnfmlem4  23900  fmfnfm  23901  lmflf  23948  txflf  23949  cnextfval  24005  cnextcn  24010  clssubg  24052  ghmcnp  24058  qustgplem  24064  tsmsval  24074  ucncn  24227  xmetdmdm  24278  metn0  24303  tmsval  24424  metustid  24497  metustexhalf  24499  metustfbas  24500  isngp2  24540  evth  24904  lmmbrf  25207  iscfil2  25211  caufval  25220  iscau2  25222  caucfil  25228  ovollb2  25434  ovolunlem1a  25441  ovoliunlem1  25447  ovoliun2  25451  ioombl1lem4  25506  uniioombllem1  25526  uniioombllem2  25528  uniioombllem6  25533  mbfconstlem  25572  ismbfcn  25574  mbfmulc2lem  25592  mbfmulc2re  25593  cncombf  25603  mbfaddlem  25605  mbflimsup  25611  i1f0rn  25627  itg1addlem5  25645  itg1climres  25659  mbfmullem2  25669  limcfval  25817  limcdif  25821  ellimc2  25822  ellimc3  25824  limccnp  25836  dvfval  25842  cpnord  25880  cpnres  25882  dvcmul  25889  dvcmulf  25890  dvexp  25898  dvgt0lem1  25948  dvcnvrelem1  25963  itgpowd  25998  plyaddlem1  26159  plymullem1  26160  plycpn  26237  aalioulem3  26282  tayl0  26309  dvntaylp  26319  ulm2  26334  ulmdvlem1  26349  xrlimcnp  26918  dchrelbas2  27188  dchrghm  27207  dchrptlem1  27215  dchrptlem2  27216  iscgrgd  28569  iscgrglt  28570  trgcgrg  28571  tgcgr4  28587  motcgrg  28600  wrdupgr  29142  wrdumgr  29154  grporndm  30570  sspn  30796  fmptcof2  32719  fnpreimac  32732  curry2ima  32771  fpwrelmap  32795  indf1ofs  32931  swrdf1  33021  pmtrcnel  33155  pmtrcnel2  33156  pmtrcnelor  33157  wrdpmtrlast  33159  cycpmcl  33182  cycpmco2f1  33190  cycpmco2rn  33191  cycpmco2lem1  33192  cycpmco2lem2  33193  cycpmco2lem3  33194  cycpmco2lem4  33195  cycpmco2lem5  33196  cycpmco2lem6  33197  cycpmco2lem7  33198  cycpmco2  33199  cyc3co2  33206  cycpmconjv  33208  fxpgaval  33233  rmfsupp2  33304  elrgspnsubrunlem2  33314  rndrhmcl  33362  elrspunidl  33493  rhmimaidl  33497  1arithidomlem2  33601  1arithidom  33602  evls1dm  33626  evlextv  33691  esplymhp  33717  esplysply  33720  esplyfval1  33722  ply1degltdimlem  33772  fldextrspunlsp  33824  irngnzply1lem  33840  irngnzply1  33841  zarcmplem  34031  rhmpreimacnlem  34034  esumpcvgval  34228  ofcfval4  34255  measdivcst  34374  oms0  34447  omsmon  34448  omssubaddlem  34449  omssubadd  34450  carsgval  34453  omsmeas  34473  sitgclg  34492  eulerpartlemgu  34527  sseqfv2  34544  rrvdm  34596  ftc2re  34748  cvmliftmolem1  35469  cvmliftlem3  35475  cvmliftlem10  35482  cvmliftlem13  35484  cvmlift2lem9  35499  cvmlift3lem6  35512  cvmlift3lem7  35513  mclsax  35757  mclsppslem  35771  mclspps  35772  fwddifval  36350  fwddifnval  36351  weiunfrlem  36652  bj-finsumval0  37597  curunc  37914  itg2addnclem2  37984  ftc1anclem5  38009  ftc1anclem6  38010  ftc1anclem8  38012  sdclem2  38054  isbnd3  38096  ssbnd  38100  bnd2lem  38103  ismtyval  38112  grpokerinj  38205  rngosn3  38236  rngodm1dm2  38244  divrngcl  38269  isdrngo2  38270  sticksstones1  42577  aks5lem2  42618  evlselvlem  43018  mapfzcons2  43150  fnwe2lem2  43482  lmhmfgima  43515  wnefimgd  44591  binomcxplemnotnn0  44786  cncmpmax  45466  mullimcf  46057  limsuppnfdlem  46133  limsupvaluz  46140  climxrrelem  46181  climxrre  46182  liminfvalxr  46215  liminflimsupxrre  46249  xlimmnfvlem2  46265  xlimpnfvlem2  46269  xlimliminflimsup  46294  cncfuni  46318  cncficcgt0  46320  cncfioobd  46329  dvsinax  46345  itgperiod  46413  fvvolioof  46421  fvvolicof  46423  stoweidlem29  46461  fourierdlem20  46559  fourierdlem53  46591  fourierdlem63  46601  fourierdlem68  46606  fourierdlem82  46620  sge0sn  46811  sge0tsms  46812  sge0cl  46813  sge0isum  46859  ismeannd  46899  hoicvr  46980  dmovn  47036  hspmbl  47061  ovolval4lem1  47081  ovnovollem1  47088  ovnovollem2  47089  issmfd  47167  issmfdf  47169  cnfsmf  47172  issmfled  47189  issmfgtd  47193  smfsuplem1  47243  smfdivdmmbl2  47273  fcores  47501  f1cof1blem  47508  f1cof1b  47511  funfocofob  47512  rmsuppss  48804  itcovalendof  49103  ffvbr  49289  lmdran  50104  cmdlan  50105