Theorem fdmd 6716

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  dom cdm 5660  ⟶wf 6532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-fn 6539  df-f 6540

This theorem is used by:  fssdmd  6724  fssdm  6725  foima  6797  focnvimacdmdm  6804  resdif  6842  fssrescdmd  7122  fmptco  7125  funfvima2d  7230  focdmex  7951  suppsnop  8172  onnseq  8329  fopwdom  9071  fodomfib  9286  intrnfi  9374  ordtypelem5  9482  ordtypelem6  9483  ordtypelem7  9484  ordtypelem8  9485  brwdomn0  9529  wdomtr  9535  fseqenlem2  10016  fin23lem30  10332  isf34lem5  10368  isf34lem7  10369  isf34lem6  10370  fin1a2lem7  10396  ttukeylem6  10504  fodomb  10516  pwxpndom2  10656  hashf1lem1  14499  wrddm  14565  ccatdmss  14626  swrdcl  14690  cats1un  14765  repswswrd  14828  limsupgle  15535  limsupgre  15539  rlim  15553  rlimi  15571  lo1o1  15590  rlimuni  15608  o1co  15644  rlimcn1  15646  ruclem11  16302  1arith  16993  ramval  17074  0ram  17086  mrcuni  17683  homarcl2  18098  prfval  18261  pfxchn  18672  chnind  18683  chnccats1  18687  chnccat  18688  gsumval  18741  gsumval2  18750  mndpsuppss  18829  frmdss2  18928  ghmrn  19305  cntzmhm2  19418  gsumval3  19983  gsumzaddlem  19997  dmdprdd  20077  dprdres  20106  dprdf1  20111  dprd2da  20120  dmdprdsplit2lem  20123  dmdprdsplit2  20124  dmdprdsplit  20125  dprdsplit  20126  dpjidcl  20136  ablfac1eulem  20150  ablfac1eu  20151  ablfaclem2  20164  ablfac2  20167  crngrhmfo  20585  lmhmlsp  21181  rhmpreimaidl  21427  frlmsslsp  21957  f1lindf  21983  mattpostpos  22622  iinopn  23070  lmbrf  23428  cnntri  23439  cnclsi  23440  lmcnp  23472  cnt0  23514  cnt1  23518  cnhaus  23522  cncmp  23560  connima  23593  1stcfb  23613  1stccnp  23630  1stckgenlem  23721  kgencn3  23726  txcnpi  23776  txcnp  23788  prdstps  23797  xkohaus  23821  xkoco2cn  23826  qtopeu  23884  hmeores  23939  fmfnfmlem2  24123  fmfnfmlem4  24125  fmfnfm  24126  lmflf  24173  txflf  24174  cnextfval  24230  cnextcn  24235  clssubg  24277  ghmcnp  24283  qustgplem  24289  tsmsval  24299  ucncn  24452  xmetdmdm  24503  metn0  24528  tmsval  24649  metustid  24722  metustexhalf  24724  metustfbas  24725  isngp2  24765  evth  25129  lmmbrf  25432  iscfil2  25436  caufval  25445  iscau2  25447  caucfil  25453  ovollb2  25659  ovolunlem1a  25666  ovoliunlem1  25672  ovoliun2  25676  ioombl1lem4  25731  uniioombllem1  25751  uniioombllem2  25753  uniioombllem6  25758  mbfconstlem  25797  ismbfcn  25799  mbfmulc2lem  25817  mbfmulc2re  25818  cncombf  25828  mbfaddlem  25830  mbflimsup  25836  i1f0rn  25852  itg1addlem5  25870  itg1climres  25884  mbfmullem2  25894  limcfval  26042  limcdif  26046  ellimc2  26047  ellimc3  26049  limccnp  26061  dvfval  26067  cpnord  26105  cpnres  26107  dvcmul  26114  dvcmulf  26115  dvexp  26123  dvgt0lem1  26172  dvcnvrelem1  26187  itgpowd  26220  plyaddlem1  26381  plymullem1  26382  plycpn  26461  aalioulem3  26508  tayl0  26536  dvntaylp  26545  ulm2  26559  ulmdvlem1  26574  xrlimcnp  27144  dchrelbas2  27412  dchrghm  27431  dchrptlem1  27439  dchrptlem2  27440  iscgrgd  28793  iscgrglt  28794  trgcgrg  28795  tgcgr4  28811  motcgrg  28824  wrdupgr  29446  wrdumgr  29458  grporndm  30873  sspn  31099  fmptcof2  33013  fnpreimac  33026  curry2ima  33065  fpwrelmap  33089  indf1ofs  33197  swrdf1  33285  pmtrcnel  33418  pmtrcnel2  33419  pmtrcnelor  33420  wrdpmtrlast  33422  cycpmcl  33445  cycpmco2f1  33453  cycpmco2rn  33454  cycpmco2lem1  33455  cycpmco2lem2  33456  cycpmco2lem3  33457  cycpmco2lem4  33458  cycpmco2lem5  33459  cycpmco2lem6  33460  cycpmco2lem7  33461  cycpmco2  33462  cyc3co2  33469  cycpmconjv  33471  fxpgaval  33496  rmfsupp2  33566  elrgspnsubrunlem2  33577  rndrhmcl  33626  elrspunidl  33745  rhmimaidl  33749  1arithidomlem2  33835  1arithidom  33836  evls1dm  33860  selvascl  33916  evlextv  33941  esplymhp  33967  esplysply  33970  esplyfval1  33972  ply1degltdimlem  34021  fldextrspunlsp  34073  irngnzply1lem  34089  irngnzply1  34090  zarcmplem  34280  rhmpreimacnlem  34283  esumpcvgval  34477  ofcfval4  34504  measdivcst  34623  oms0  34696  omsmon  34697  omssubaddlem  34698  omssubadd  34699  carsgval  34702  omsmeas  34722  sitgclg  34741  eulerpartlemgu  34776  sseqfv2  34793  rrvdm  34845  ftc2re  34994  cvmliftmolem1  35781  cvmliftlem3  35787  cvmliftlem10  35794  cvmliftlem13  35796  cvmlift2lem9  35811  cvmlift3lem6  35824  cvmlift3lem7  35825  mclsax  36069  mclsppslem  36083  mclspps  36084  fwddifval  36662  fwddifnval  36663  weiunfrlem  37003  bj-finsumval0  37957  curunc  38281  itg2addnclem2  38351  ftc1anclem5  38376  ftc1anclem6  38377  ftc1anclem8  38379  sdclem2  38421  isbnd3  38463  ssbnd  38467  bnd2lem  38470  ismtyval  38479  grpokerinj  38572  rngosn3  38603  rngodm1dm2  38611  divrngcl  38636  isdrngo2  38637  sticksstones1  42941  aks5lem2  42982  evlselvlem  43348  mapfzcons2  43478  fnwe2lem2  43806  lmhmfgima  43839  wnefimgd  44915  binomcxplemnotnn0  45094  cncmpmax  45780  mullimcf  46367  limsuppnfdlem  46443  limsupvaluz  46450  climxrrelem  46491  climxrre  46492  liminfvalxr  46525  liminflimsupxrre  46559  xlimmnfvlem2  46575  xlimpnfvlem2  46579  xlimliminflimsup  46604  cncfuni  46628  cncficcgt0  46630  cncfioobd  46639  dvsinax  46655  itgperiod  46723  fvvolioof  46731  fvvolicof  46733  stoweidlem29  46771  fourierdlem20  46869  fourierdlem48  46896  fourierdlem49  46897  fourierdlem53  46901  fourierdlem63  46911  fourierdlem68  46916  fourierdlem82  46930  fourierdlem113  46961  sge0sn  47121  sge0tsms  47122  sge0cl  47123  sge0isum  47169  ismeannd  47209  hoicvr  47290  dmovn  47346  hspmbl  47371  ovolval4lem1  47391  ovnovollem1  47398  ovnovollem2  47399  issmfd  47477  issmfdf  47479  cnfsmf  47482  issmfled  47499  issmfgtd  47503  smfsuplem1  47553  smfdivdmmbl2  47583  fcores  47832  f1cof1blem  47839  f1cof1b  47842  funfocofob  47843  rmsuppss  49178  itcovalendof  49477  ffvbr  49662  lmdran  50477  cmdlan  50478