Theorem fdmd 6657

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

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5614  ⟶wf 6473

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 6480  df-f 6481

This theorem is referenced by:  fssdmd  6665  fssdm  6666  foima  6736  focnvimacdmdm  6743  resdif  6780  fssrescdmd  7054  fmptco  7057  funfvima2d  7161  focdmex  7883  suppsnop  8103  onnseq  8259  fopwdom  8993  fodomfib  9208  fodomfibOLD  9210  intrnfi  9295  ordtypelem5  9403  ordtypelem6  9404  ordtypelem7  9405  ordtypelem8  9406  brwdomn0  9450  wdomtr  9456  fseqenlem2  9908  fin23lem30  10225  isf34lem5  10261  isf34lem7  10262  isf34lem6  10263  fin1a2lem7  10289  ttukeylem6  10397  fodomb  10409  pwxpndom2  10548  hashf1lem1  14354  wrddm  14420  ccatdmss  14481  swrdcl  14545  cats1un  14620  repswswrd  14683  limsupgle  15376  limsupgre  15380  rlim  15394  rlimi  15412  lo1o1  15431  rlimuni  15449  o1co  15485  rlimcn1  15487  ruclem11  16141  1arith  16831  ramval  16912  0ram  16924  mrcuni  17519  homarcl2  17934  prfval  18097  pfxchn  18508  chnind  18519  chnccats1  18523  chnccat  18524  gsumval  18577  gsumval2  18586  mndpsuppss  18665  frmdss2  18763  ghmrn  19134  cntzmhm2  19247  gsumval3  19812  gsumzaddlem  19826  dmdprdd  19906  dprdres  19935  dprdf1  19940  dprd2da  19949  dmdprdsplit2lem  19952  dmdprdsplit2  19953  dmdprdsplit  19954  dprdsplit  19955  dpjidcl  19965  ablfac1eulem  19979  ablfac1eu  19980  ablfaclem2  19993  ablfac2  19996  lmhmlsp  20976  rhmpreimaidl  21207  frlmsslsp  21726  f1lindf  21752  mattpostpos  22362  iinopn  22810  lmbrf  23168  cnntri  23179  cnclsi  23180  lmcnp  23212  cnt0  23254  cnt1  23258  cnhaus  23262  cncmp  23300  connima  23333  1stcfb  23353  1stccnp  23370  1stckgenlem  23461  kgencn3  23466  txcnpi  23516  txcnp  23528  prdstps  23537  xkohaus  23561  xkoco2cn  23566  qtopeu  23624  hmeores  23679  fmfnfmlem2  23863  fmfnfmlem4  23865  fmfnfm  23866  lmflf  23913  txflf  23914  cnextfval  23970  cnextcn  23975  clssubg  24017  ghmcnp  24023  qustgplem  24029  tsmsval  24039  ucncn  24192  xmetdmdm  24243  metn0  24268  tmsval  24389  metustid  24462  metustexhalf  24464  metustfbas  24465  isngp2  24505  evth  24878  lmmbrf  25182  iscfil2  25186  caufval  25195  iscau2  25197  caucfil  25203  ovollb2  25410  ovolunlem1a  25417  ovoliunlem1  25423  ovoliun2  25427  ioombl1lem4  25482  uniioombllem1  25502  uniioombllem2  25504  uniioombllem6  25509  mbfconstlem  25548  ismbfcn  25550  mbfmulc2lem  25568  mbfmulc2re  25569  cncombf  25579  mbfaddlem  25581  mbflimsup  25587  i1f0rn  25603  itg1addlem5  25621  itg1climres  25635  mbfmullem2  25645  limcfval  25793  limcdif  25797  ellimc2  25798  ellimc3  25800  limccnp  25812  dvfval  25818  cpnord  25857  cpnres  25859  dvcmul  25867  dvcmulf  25868  dvexp  25877  dvgt0lem1  25927  dvcnvrelem1  25942  itgpowd  25977  plyaddlem1  26138  plymullem1  26139  plycpn  26217  aalioulem3  26262  tayl0  26289  dvntaylp  26299  ulm2  26314  ulmdvlem1  26329  xrlimcnp  26898  dchrelbas2  27168  dchrghm  27187  dchrptlem1  27195  dchrptlem2  27196  iscgrgd  28484  iscgrglt  28485  trgcgrg  28486  tgcgr4  28502  motcgrg  28515  wrdupgr  29056  wrdumgr  29068  grporndm  30480  sspn  30706  fmptcof2  32629  fnpreimac  32643  curry2ima  32680  fpwrelmap  32706  indf1ofs  32837  swrdf1  32927  pmtrcnel  33048  pmtrcnel2  33049  pmtrcnelor  33050  wrdpmtrlast  33052  cycpmcl  33075  cycpmco2f1  33083  cycpmco2rn  33084  cycpmco2lem1  33085  cycpmco2lem2  33086  cycpmco2lem3  33087  cycpmco2lem4  33088  cycpmco2lem5  33089  cycpmco2lem6  33090  cycpmco2lem7  33091  cycpmco2  33092  cyc3co2  33099  cycpmconjv  33101  fxpgaval  33126  rmfsupp2  33195  elrgspnsubrunlem2  33205  rndrhmcl  33252  elrspunidl  33383  rhmimaidl  33387  1arithidomlem2  33491  1arithidom  33492  evls1dm  33514  esplymhp  33579  esplysply  33582  ply1degltdimlem  33625  fldextrspunlsp  33677  irngnzply1lem  33693  irngnzply1  33694  zarcmplem  33884  rhmpreimacnlem  33887  esumpcvgval  34081  ofcfval4  34108  measdivcst  34227  oms0  34300  omsmon  34301  omssubaddlem  34302  omssubadd  34303  carsgval  34306  omsmeas  34326  sitgclg  34345  eulerpartlemgu  34380  sseqfv2  34397  rrvdm  34449  ftc2re  34601  cvmliftmolem1  35293  cvmliftlem3  35299  cvmliftlem10  35306  cvmliftlem13  35308  cvmlift2lem9  35323  cvmlift3lem6  35336  cvmlift3lem7  35337  mclsax  35581  mclsppslem  35595  mclspps  35596  fwddifval  36175  fwddifnval  36176  weiunfrlem  36477  bj-finsumval0  37298  curunc  37621  itg2addnclem2  37691  ftc1anclem5  37716  ftc1anclem6  37717  ftc1anclem8  37719  sdclem2  37761  isbnd3  37803  ssbnd  37807  bnd2lem  37810  ismtyval  37819  grpokerinj  37912  rngosn3  37943  rngodm1dm2  37951  divrngcl  37976  isdrngo2  37977  sticksstones1  42158  aks5lem2  42199  evlselvlem  42598  mapfzcons2  42731  fnwe2lem2  43063  lmhmfgima  43096  wnefimgd  44173  binomcxplemnotnn0  44368  cncmpmax  45048  mullimcf  45642  limsuppnfdlem  45718  limsupvaluz  45725  climxrrelem  45766  climxrre  45767  liminfvalxr  45800  liminflimsupxrre  45834  xlimmnfvlem2  45850  xlimpnfvlem2  45854  xlimliminflimsup  45879  cncfuni  45903  cncficcgt0  45905  cncfioobd  45914  dvsinax  45930  itgperiod  45998  fvvolioof  46006  fvvolicof  46008  stoweidlem29  46046  fourierdlem20  46144  fourierdlem53  46176  fourierdlem63  46186  fourierdlem68  46191  fourierdlem82  46205  sge0sn  46396  sge0tsms  46397  sge0cl  46398  sge0isum  46444  ismeannd  46484  hoicvr  46565  dmovn  46621  hspmbl  46646  ovolval4lem1  46666  ovnovollem1  46673  ovnovollem2  46674  issmfd  46752  issmfdf  46754  cnfsmf  46757  issmfled  46774  issmfgtd  46778  smfsuplem1  46828  smfdivdmmbl2  46858  fcores  47077  f1cof1blem  47084  f1cof1b  47087  funfocofob  47088  rmsuppss  48380  itcovalendof  48680  ffvbr  48866  lmdran  49682  cmdlan  49683