Theorem fdmd 6746

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

Syntax hints:   → wi 4   = wceq 1536  dom cdm 5688  ⟶wf 6558

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 6565  df-f 6566

This theorem is referenced by:  fssdmd  6754  fssdm  6755  foima  6825  focnvimacdmdm  6832  resdif  6869  fssrescdmd  7145  fmptco  7148  funfvima2d  7251  focdmex  7978  suppsnop  8201  onnseq  8382  fopwdom  9118  fodomfib  9366  fodomfibOLD  9368  intrnfi  9453  ordtypelem5  9559  ordtypelem6  9560  ordtypelem7  9561  ordtypelem8  9562  brwdomn0  9606  wdomtr  9612  fseqenlem2  10062  fin23lem30  10379  isf34lem5  10415  isf34lem7  10416  isf34lem6  10417  fin1a2lem7  10443  ttukeylem6  10551  fodomb  10563  pwxpndom2  10702  hashf1lem1  14490  wrddm  14555  swrdcl  14679  cats1un  14755  repswswrd  14818  limsupgle  15509  limsupgre  15513  rlim  15527  rlimi  15545  lo1o1  15564  rlimuni  15582  o1co  15618  rlimcn1  15620  ruclem11  16272  1arith  16960  ramval  17041  0ram  17053  mrcuni  17665  homarcl2  18088  prfval  18254  gsumval  18702  gsumval2  18711  mndpsuppss  18790  frmdss2  18888  ghmrn  19259  cntzmhm2  19372  gsumval3  19939  gsumzaddlem  19953  dmdprdd  20033  dprdres  20062  dprdf1  20067  dprd2da  20076  dmdprdsplit2lem  20079  dmdprdsplit2  20080  dmdprdsplit  20081  dprdsplit  20082  dpjidcl  20092  ablfac1eulem  20106  ablfac1eu  20107  ablfaclem2  20120  ablfac2  20123  lmhmlsp  21065  rhmpreimaidl  21304  frlmsslsp  21833  f1lindf  21859  mattpostpos  22475  iinopn  22923  lmbrf  23283  cnntri  23294  cnclsi  23295  lmcnp  23327  cnt0  23369  cnt1  23373  cnhaus  23377  cncmp  23415  connima  23448  1stcfb  23468  1stccnp  23485  1stckgenlem  23576  kgencn3  23581  txcnpi  23631  txcnp  23643  prdstps  23652  xkohaus  23676  xkoco2cn  23681  qtopeu  23739  hmeores  23794  fmfnfmlem2  23978  fmfnfmlem4  23980  fmfnfm  23981  lmflf  24028  txflf  24029  cnextfval  24085  cnextcn  24090  clssubg  24132  ghmcnp  24138  qustgplem  24144  tsmsval  24154  ucncn  24309  xmetdmdm  24360  metn0  24385  tmsval  24508  metustid  24582  metustexhalf  24584  metustfbas  24585  isngp2  24625  evth  25004  lmmbrf  25309  iscfil2  25313  caufval  25322  iscau2  25324  caucfil  25330  ovollb2  25537  ovolunlem1a  25544  ovoliunlem1  25550  ovoliun2  25554  ioombl1lem4  25609  uniioombllem1  25629  uniioombllem2  25631  uniioombllem6  25636  mbfconstlem  25675  ismbfcn  25677  mbfmulc2lem  25695  mbfmulc2re  25696  cncombf  25706  mbfaddlem  25708  mbflimsup  25714  i1f0rn  25730  itg1addlem5  25749  itg1climres  25763  mbfmullem2  25773  limcfval  25921  limcdif  25925  ellimc2  25926  ellimc3  25928  limccnp  25940  dvfval  25946  cpnord  25985  cpnres  25987  dvcmul  25995  dvcmulf  25996  dvexp  26005  dvgt0lem1  26055  dvcnvrelem1  26070  itgpowd  26105  plyaddlem1  26266  plymullem1  26267  plycpn  26345  aalioulem3  26390  tayl0  26417  dvntaylp  26427  ulm2  26442  ulmdvlem1  26457  xrlimcnp  27025  dchrelbas2  27295  dchrghm  27314  dchrptlem1  27322  dchrptlem2  27323  iscgrgd  28535  iscgrglt  28536  trgcgrg  28537  tgcgr4  28553  motcgrg  28566  wrdupgr  29116  wrdumgr  29128  grporndm  30538  sspn  30764  fmptcof2  32673  fnpreimac  32687  curry2ima  32723  fpwrelmap  32750  ccatdmss  32918  swrdf1  32925  pfxchn  32983  chnind  32984  pmtrcnel  33091  pmtrcnel2  33092  pmtrcnelor  33093  wrdpmtrlast  33095  cycpmcl  33118  cycpmco2f1  33126  cycpmco2rn  33127  cycpmco2lem1  33128  cycpmco2lem2  33129  cycpmco2lem3  33130  cycpmco2lem4  33131  cycpmco2lem5  33132  cycpmco2lem6  33133  cycpmco2lem7  33134  cycpmco2  33135  cyc3co2  33142  cycpmconjv  33144  rmfsupp2  33227  rndrhmcl  33279  elrspunidl  33435  rhmimaidl  33439  1arithidomlem2  33543  1arithidom  33544  evls1dm  33566  ply1degltdimlem  33649  irngnzply1lem  33704  irngnzply1  33705  zarcmplem  33841  rhmpreimacnlem  33844  indf1ofs  34006  esumpcvgval  34058  ofcfval4  34085  measdivcst  34204  oms0  34278  omsmon  34279  omssubaddlem  34280  omssubadd  34281  carsgval  34284  omsmeas  34304  sitgclg  34323  eulerpartlemgu  34358  sseqfv2  34375  rrvdm  34427  ftc2re  34591  cvmliftmolem1  35265  cvmliftlem3  35271  cvmliftlem10  35278  cvmliftlem13  35280  cvmlift2lem9  35295  cvmlift3lem6  35308  cvmlift3lem7  35309  mclsax  35553  mclsppslem  35567  mclspps  35568  fwddifval  36143  fwddifnval  36144  weiunfrlem  36446  bj-finsumval0  37267  curunc  37588  itg2addnclem2  37658  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anclem8  37686  sdclem2  37728  isbnd3  37770  ssbnd  37774  bnd2lem  37777  ismtyval  37786  grpokerinj  37879  rngosn3  37910  rngodm1dm2  37918  divrngcl  37943  isdrngo2  37944  sticksstones1  42127  aks5lem2  42168  evlselvlem  42572  mapfzcons2  42706  fnwe2lem2  43039  lmhmfgima  43072  wnefimgd  44150  binomcxplemnotnn0  44351  cncmpmax  44969  mullimcf  45578  limsuppnfdlem  45656  limsupvaluz  45663  climxrrelem  45704  climxrre  45705  liminfvalxr  45738  liminflimsupxrre  45772  xlimmnfvlem2  45788  xlimpnfvlem2  45792  xlimliminflimsup  45817  cncfuni  45841  cncficcgt0  45843  cncfioobd  45852  dvsinax  45868  itgperiod  45936  fvvolioof  45944  fvvolicof  45946  stoweidlem29  45984  fourierdlem20  46082  fourierdlem53  46114  fourierdlem63  46124  fourierdlem68  46129  fourierdlem82  46143  sge0sn  46334  sge0tsms  46335  sge0cl  46336  sge0isum  46382  ismeannd  46422  hoicvr  46503  dmovn  46559  hspmbl  46584  ovolval4lem1  46604  ovnovollem1  46611  ovnovollem2  46612  issmfd  46690  issmfdf  46692  cnfsmf  46695  issmfled  46712  issmfgtd  46716  smfsuplem1  46766  smfdivdmmbl2  46796  fcores  47016  f1cof1blem  47023  f1cof1b  47026  funfocofob  47027  rmsuppss  48214  itcovalendof  48518