Theorem fdmd 6727

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

Syntax hints:   → wi 4   = wceq 1534  dom cdm 5672  ⟶wf 6538

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 396  df-fn 6545  df-f 6546

This theorem is referenced by:  fssdmd  6735  fssdm  6736  foima  6810  focnvimacdmdm  6817  resdif  6854  fmptco  7132  funfvima2d  7238  focdmex  7953  suppsnop  8176  onnseq  8358  fopwdom  9096  fodomfib  9342  intrnfi  9431  ordtypelem5  9537  ordtypelem6  9538  ordtypelem7  9539  ordtypelem8  9540  brwdomn0  9584  wdomtr  9590  fseqenlem2  10040  fin23lem30  10357  isf34lem5  10393  isf34lem7  10394  isf34lem6  10395  fin1a2lem7  10421  ttukeylem6  10529  fodomb  10541  pwxpndom2  10680  hashf1lem1  14439  hashf1lem1OLD  14440  wrddm  14495  swrdcl  14619  cats1un  14695  repswswrd  14758  limsupgle  15445  limsupgre  15449  rlim  15463  rlimi  15481  lo1o1  15500  rlimuni  15518  o1co  15554  rlimcn1  15556  ruclem11  16208  1arith  16887  ramval  16968  0ram  16980  mrcuni  17592  homarcl2  18015  prfval  18181  gsumval  18628  gsumval2  18637  frmdss2  18806  ghmrn  19174  cntzmhm2  19284  gsumval3  19853  gsumzaddlem  19867  dmdprdd  19947  dprdres  19976  dprdf1  19981  dprd2da  19990  dmdprdsplit2lem  19993  dmdprdsplit2  19994  dmdprdsplit  19995  dprdsplit  19996  dpjidcl  20006  ablfac1eulem  20020  ablfac1eu  20021  ablfaclem2  20034  ablfac2  20037  lmhmlsp  20923  frlmsslsp  21717  f1lindf  21743  mattpostpos  22343  iinopn  22791  lmbrf  23151  cnntri  23162  cnclsi  23163  lmcnp  23195  cnt0  23237  cnt1  23241  cnhaus  23245  cncmp  23283  connima  23316  1stcfb  23336  1stccnp  23353  1stckgenlem  23444  kgencn3  23449  txcnpi  23499  txcnp  23511  prdstps  23520  xkohaus  23544  xkoco2cn  23549  qtopeu  23607  hmeores  23662  fmfnfmlem2  23846  fmfnfmlem4  23848  fmfnfm  23849  lmflf  23896  txflf  23897  cnextfval  23953  cnextcn  23958  clssubg  24000  ghmcnp  24006  qustgplem  24012  tsmsval  24022  ucncn  24177  xmetdmdm  24228  metn0  24253  tmsval  24376  metustid  24450  metustexhalf  24452  metustfbas  24453  isngp2  24493  evth  24872  lmmbrf  25177  iscfil2  25181  caufval  25190  iscau2  25192  caucfil  25198  ovollb2  25405  ovolunlem1a  25412  ovoliunlem1  25418  ovoliun2  25422  ioombl1lem4  25477  uniioombllem1  25497  uniioombllem2  25499  uniioombllem6  25504  mbfconstlem  25543  ismbfcn  25545  mbfmulc2lem  25563  mbfmulc2re  25564  cncombf  25574  mbfaddlem  25576  mbflimsup  25582  i1f0rn  25598  itg1addlem5  25617  itg1climres  25631  mbfmullem2  25641  limcfval  25788  limcdif  25792  ellimc2  25793  ellimc3  25795  limccnp  25807  dvfval  25813  cpnord  25852  cpnres  25854  dvcmul  25862  dvcmulf  25863  dvexp  25872  dvgt0lem1  25922  dvcnvrelem1  25937  itgpowd  25972  plyaddlem1  26134  plymullem1  26135  plycpn  26211  aalioulem3  26256  tayl0  26283  dvntaylp  26293  ulm2  26308  ulmdvlem1  26323  xrlimcnp  26887  dchrelbas2  27157  dchrghm  27176  dchrptlem1  27184  dchrptlem2  27185  iscgrgd  28304  iscgrglt  28305  trgcgrg  28306  tgcgr4  28322  motcgrg  28335  wrdupgr  28885  wrdumgr  28897  grporndm  30307  sspn  30533  fmptcof2  32426  fnpreimac  32440  curry2ima  32472  fpwrelmap  32499  swrdf1  32659  pmtrcnel  32790  pmtrcnel2  32791  pmtrcnelor  32792  cycpmcl  32815  cycpmco2f1  32823  cycpmco2rn  32824  cycpmco2lem1  32825  cycpmco2lem2  32826  cycpmco2lem3  32827  cycpmco2lem4  32828  cycpmco2lem5  32829  cycpmco2lem6  32830  cycpmco2lem7  32831  cycpmco2  32832  cyc3co2  32839  cycpmconjv  32841  rmfsupp2  32923  rndrhmcl  32933  rhmpreimaidl  33070  elrspunidl  33079  rhmimaidl  33083  evls1dm  33172  ply1degltdimlem  33252  irngnzply1lem  33300  irngnzply1  33301  zarcmplem  33418  rhmpreimacnlem  33421  indf1ofs  33581  esumpcvgval  33633  ofcfval4  33660  measdivcst  33779  oms0  33853  omsmon  33854  omssubaddlem  33855  omssubadd  33856  carsgval  33859  omsmeas  33879  sitgclg  33898  eulerpartlemgu  33933  sseqfv2  33950  rrvdm  34002  ftc2re  34166  cvmliftmolem1  34827  cvmliftlem3  34833  cvmliftlem10  34840  cvmliftlem13  34842  cvmlift2lem9  34857  cvmlift3lem6  34870  cvmlift3lem7  34871  mclsax  35115  mclsppslem  35129  mclspps  35130  fwddifval  35694  fwddifnval  35695  bj-finsumval0  36700  curunc  37010  itg2addnclem2  37080  ftc1anclem5  37105  ftc1anclem6  37106  ftc1anclem8  37108  sdclem2  37150  isbnd3  37192  ssbnd  37196  bnd2lem  37199  ismtyval  37208  grpokerinj  37301  rngosn3  37332  rngodm1dm2  37340  divrngcl  37365  isdrngo2  37366  sticksstones1  41550  evlselvlem  41741  mapfzcons2  42061  fnwe2lem2  42397  lmhmfgima  42430  wnefimgd  43514  binomcxplemnotnn0  43716  cncmpmax  44317  mullimcf  44934  limsuppnfdlem  45012  limsupvaluz  45019  climxrrelem  45060  climxrre  45061  liminfvalxr  45094  liminflimsupxrre  45128  xlimmnfvlem2  45144  xlimpnfvlem2  45148  xlimliminflimsup  45173  cncfuni  45197  cncficcgt0  45199  cncfioobd  45208  dvsinax  45224  itgperiod  45292  fvvolioof  45300  fvvolicof  45302  stoweidlem29  45340  fourierdlem20  45438  fourierdlem53  45470  fourierdlem63  45480  fourierdlem68  45485  fourierdlem82  45499  sge0sn  45690  sge0tsms  45691  sge0cl  45692  sge0isum  45738  ismeannd  45778  hoicvr  45859  dmovn  45915  hspmbl  45940  ovolval4lem1  45960  ovnovollem1  45967  ovnovollem2  45968  issmfd  46046  issmfdf  46048  cnfsmf  46051  issmfled  46068  issmfgtd  46072  smfsuplem1  46122  smfdivdmmbl2  46152  fcores  46372  f1cof1blem  46379  f1cof1b  46380  funfocofob  46381  rmsuppss  47357  mndpsuppss  47358  itcovalendof  47665