Theorem fdmd 6725

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

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5675  ⟶wf 6536

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 397  df-fn 6543  df-f 6544

This theorem is referenced by:  fssdmd  6733  fssdm  6734  foima  6807  focnvimacdmdm  6814  resdif  6851  fmptco  7123  funfvima2d  7230  focdmex  7938  suppsnop  8159  onnseq  8340  fopwdom  9076  fodomfib  9322  intrnfi  9407  ordtypelem5  9513  ordtypelem6  9514  ordtypelem7  9515  ordtypelem8  9516  brwdomn0  9560  wdomtr  9566  fseqenlem2  10016  fin23lem30  10333  isf34lem5  10369  isf34lem7  10370  isf34lem6  10371  fin1a2lem7  10397  ttukeylem6  10505  fodomb  10517  pwxpndom2  10656  hashf1lem1  14411  hashf1lem1OLD  14412  wrddm  14467  swrdcl  14591  cats1un  14667  repswswrd  14730  limsupgle  15417  limsupgre  15421  rlim  15435  rlimi  15453  lo1o1  15472  rlimuni  15490  o1co  15526  rlimcn1  15528  ruclem11  16179  1arith  16856  ramval  16937  0ram  16949  mrcuni  17561  homarcl2  17981  prfval  18147  gsumval  18592  gsumval2  18601  frmdss2  18740  ghmrn  19099  cntzmhm2  19200  gsumval3  19769  gsumzaddlem  19783  dmdprdd  19863  dprdres  19892  dprdf1  19897  dprd2da  19906  dmdprdsplit2lem  19909  dmdprdsplit2  19910  dmdprdsplit  19911  dprdsplit  19912  dpjidcl  19922  ablfac1eulem  19936  ablfac1eu  19937  ablfaclem2  19950  ablfac2  19953  lmhmlsp  20652  frlmsslsp  21342  f1lindf  21368  mattpostpos  21947  iinopn  22395  lmbrf  22755  cnntri  22766  cnclsi  22767  lmcnp  22799  cnt0  22841  cnt1  22845  cnhaus  22849  cncmp  22887  connima  22920  1stcfb  22940  1stccnp  22957  1stckgenlem  23048  kgencn3  23053  txcnpi  23103  txcnp  23115  prdstps  23124  xkohaus  23148  xkoco2cn  23153  qtopeu  23211  hmeores  23266  fmfnfmlem2  23450  fmfnfmlem4  23452  fmfnfm  23453  lmflf  23500  txflf  23501  cnextfval  23557  cnextcn  23562  clssubg  23604  ghmcnp  23610  qustgplem  23616  tsmsval  23626  ucncn  23781  xmetdmdm  23832  metn0  23857  tmsval  23980  metustid  24054  metustexhalf  24056  metustfbas  24057  isngp2  24097  evth  24466  lmmbrf  24770  iscfil2  24774  caufval  24783  iscau2  24785  caucfil  24791  ovollb2  24997  ovolunlem1a  25004  ovoliunlem1  25010  ovoliun2  25014  ioombl1lem4  25069  uniioombllem1  25089  uniioombllem2  25091  uniioombllem6  25096  mbfconstlem  25135  ismbfcn  25137  mbfmulc2lem  25155  mbfmulc2re  25156  cncombf  25166  mbfaddlem  25168  mbflimsup  25174  i1f0rn  25190  itg1addlem5  25209  itg1climres  25223  mbfmullem2  25233  limcfval  25380  limcdif  25384  ellimc2  25385  ellimc3  25387  limccnp  25399  dvfval  25405  cpnord  25443  cpnres  25445  dvcmul  25452  dvcmulf  25453  dvexp  25461  dvgt0lem1  25510  dvcnvrelem1  25525  itgpowd  25558  plyaddlem1  25718  plymullem1  25719  plycpn  25793  aalioulem3  25838  tayl0  25865  dvntaylp  25874  ulm2  25888  ulmdvlem1  25903  xrlimcnp  26462  dchrelbas2  26729  dchrghm  26748  dchrptlem1  26756  dchrptlem2  26757  iscgrgd  27753  iscgrglt  27754  trgcgrg  27755  tgcgr4  27771  motcgrg  27784  wrdupgr  28334  wrdumgr  28346  grporndm  29750  sspn  29976  fmptcof2  31869  fnpreimac  31883  curry2ima  31917  fpwrelmap  31945  swrdf1  32107  pmtrcnel  32237  pmtrcnel2  32238  pmtrcnelor  32239  cycpmcl  32262  cycpmco2f1  32270  cycpmco2rn  32271  cycpmco2lem1  32272  cycpmco2lem2  32273  cycpmco2lem3  32274  cycpmco2lem4  32275  cycpmco2lem5  32276  cycpmco2lem6  32277  cycpmco2lem7  32278  cycpmco2  32279  cyc3co2  32286  cycpmconjv  32288  rmfsupp2  32375  rndrhmcl  32384  rhmpreimaidl  32525  elrspunidl  32534  rhmimaidl  32538  evls1dm  32629  ply1degltdimlem  32695  irngnzply1lem  32742  irngnzply1  32743  zarcmplem  32849  rhmpreimacnlem  32852  indf1ofs  33012  esumpcvgval  33064  ofcfval4  33091  measdivcst  33210  oms0  33284  omsmon  33285  omssubaddlem  33286  omssubadd  33287  carsgval  33290  omsmeas  33310  sitgclg  33329  eulerpartlemgu  33364  sseqfv2  33381  rrvdm  33433  ftc2re  33598  cvmliftmolem1  34260  cvmliftlem3  34266  cvmliftlem10  34273  cvmliftlem13  34275  cvmlift2lem9  34290  cvmlift3lem6  34303  cvmlift3lem7  34304  mclsax  34548  mclsppslem  34562  mclspps  34563  fwddifval  35122  fwddifnval  35123  bj-finsumval0  36154  curunc  36458  itg2addnclem2  36528  ftc1anclem5  36553  ftc1anclem6  36554  ftc1anclem8  36556  sdclem2  36598  isbnd3  36640  ssbnd  36644  bnd2lem  36647  ismtyval  36656  grpokerinj  36749  rngosn3  36780  rngodm1dm2  36788  divrngcl  36813  isdrngo2  36814  sticksstones1  40950  evlselvlem  41155  mapfzcons2  41442  fnwe2lem2  41778  lmhmfgima  41811  wnefimgd  42898  binomcxplemnotnn0  43100  cncmpmax  43701  mullimcf  44325  limsuppnfdlem  44403  limsupvaluz  44410  climxrrelem  44451  climxrre  44452  liminfvalxr  44485  liminflimsupxrre  44519  xlimmnfvlem2  44535  xlimpnfvlem2  44539  xlimliminflimsup  44564  cncfuni  44588  cncficcgt0  44590  cncfioobd  44599  dvsinax  44615  itgperiod  44683  fvvolioof  44691  fvvolicof  44693  stoweidlem29  44731  fourierdlem20  44829  fourierdlem53  44861  fourierdlem63  44871  fourierdlem68  44876  fourierdlem82  44890  sge0sn  45081  sge0tsms  45082  sge0cl  45083  sge0isum  45129  ismeannd  45169  hoicvr  45250  dmovn  45306  hspmbl  45331  ovolval4lem1  45351  ovnovollem1  45358  ovnovollem2  45359  issmfd  45437  issmfdf  45439  cnfsmf  45442  issmfled  45459  issmfgtd  45463  smfsuplem1  45513  smfdivdmmbl2  45543  fcores  45763  f1cof1blem  45770  f1cof1b  45771  funfocofob  45772  rmsuppss  46999  mndpsuppss  47000  itcovalendof  47308