Theorem fdmd 6300

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

Syntax hints:   → wi 4   = wceq 1601  dom cdm 5355  ⟶wf 6131

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 199  df-an 387  df-fn 6138  df-f 6139

This theorem is referenced by:  fssdmd  6306  fssdm  6307  foima  6371  resdif  6411  fmptco  6661  fornex  7414  onnseq  7724  fopwdom  8356  fodomfib  8528  intrnfi  8610  ordtypelem5  8716  ordtypelem6  8717  ordtypelem7  8718  ordtypelem8  8719  brwdomn0  8763  wdomtr  8769  fseqenlem2  9181  fin23lem30  9499  isf34lem5  9535  isf34lem7  9536  isf34lem6  9537  fin1a2lem7  9563  ttukeylem6  9671  fodomb  9683  pwxpndom2  9822  hashf1lem1  13553  wrddm  13606  swrdcl  13735  cats1un  13841  repswswrd  13930  limsupgle  14616  limsupgre  14620  rlim  14634  rlimi  14652  lo1o1  14671  rlimuni  14689  o1co  14725  rlimcn1  14727  ruclem11  15373  1arith  16035  ramval  16116  0ram  16128  mrcuni  16667  homarcl2  17070  prfval  17225  gsumval  17657  gsumval2  17666  frmdss2  17787  ghmrn  18057  cntzmhm2  18155  gsumval3  18694  gsumzaddlem  18707  dmdprdd  18785  dprdres  18814  dprdf1  18819  dprd2da  18828  dmdprdsplit2lem  18831  dmdprdsplit2  18832  dmdprdsplit  18833  dprdsplit  18834  dpjidcl  18844  ablfac1eulem  18858  ablfac1eu  18859  ablfaclem2  18872  ablfac2  18875  lmhmlsp  19444  f1lindf  20565  mattpostpos  20665  iinopn  21114  lmbrf  21472  cnntri  21483  cnclsi  21484  lmcnp  21516  cnt0  21558  cnt1  21562  cnhaus  21566  cncmp  21604  connima  21637  1stcfb  21657  1stccnp  21674  1stckgenlem  21765  kgencn3  21770  txcnpi  21820  txcnp  21832  prdstps  21841  xkohaus  21865  xkoco2cn  21870  qtopeu  21928  hmeores  21983  fmfnfmlem2  22167  fmfnfmlem4  22169  fmfnfm  22170  lmflf  22217  txflf  22218  cnextfval  22274  cnextcn  22279  clssubg  22320  ghmcnp  22326  qustgplem  22332  tsmsval  22342  ucncn  22497  xmetdmdm  22548  metn0  22573  tmsval  22694  metustid  22767  metustexhalf  22769  metustfbas  22770  isngp2  22809  evth  23166  lmmbrf  23468  iscfil2  23472  caufval  23481  iscau2  23483  caucfil  23489  ovollb2  23693  ovolunlem1a  23700  ovoliunlem1  23706  ovoliun2  23710  ioombl1lem4  23765  uniioombllem1  23785  uniioombllem2  23787  uniioombllem6  23792  mbfconstlem  23831  ismbfcn  23833  mbfmulc2lem  23851  mbfmulc2re  23852  cncombf  23862  mbfaddlem  23864  mbflimsup  23870  i1f0rn  23886  itg1addlem5  23904  itg1climres  23918  mbfmullem2  23928  limcfval  24073  limcdif  24077  ellimc2  24078  ellimc3  24080  limccnp  24092  dvfval  24098  cpnord  24135  cpnres  24137  dvcmul  24144  dvcmulf  24145  dvexp  24153  dvgt0lem1  24202  dvcnvrelem1  24217  plyaddlem1  24406  plymullem1  24407  plycpn  24481  aalioulem3  24526  tayl0  24553  dvntaylp  24562  ulm2  24576  ulmdvlem1  24591  xrlimcnp  25147  dchrelbas2  25414  dchrghm  25433  dchrptlem1  25441  dchrptlem2  25442  iscgrgd  25864  iscgrglt  25865  trgcgrg  25866  tgcgr4  25882  motcgrg  25895  wrdupgr  26433  wrdumgr  26445  upgr1e  26461  grporndm  27937  sspn  28163  fmptcof2  30022  fnpreimac  30036  curry2ima  30052  fpwrelmap  30074  indf1ofs  30686  esumpcvgval  30738  ofcfval4  30765  measdivcst  30886  oms0  30957  omsmon  30958  omssubaddlem  30959  omssubadd  30960  carsgval  30963  omsmeas  30983  sitgclg  31002  eulerpartlemgu  31037  sseqfv2  31055  rrvdm  31107  ftc2re  31278  cvmliftmolem1  31862  cvmliftlem3  31868  cvmliftlem10  31875  cvmliftlem13  31877  cvmlift2lem9  31892  cvmlift3lem6  31905  cvmlift3lem7  31906  mclsax  32065  mclsppslem  32079  mclspps  32080  fwddifval  32858  fwddifnval  32859  bj-finsumval0  33749  curunc  34016  itg2addnclem2  34087  ftc1anclem5  34114  ftc1anclem6  34115  ftc1anclem8  34117  sdclem2  34162  isbnd3  34207  ssbnd  34211  bnd2lem  34214  ismtyval  34223  grpokerinj  34316  rngosn3  34347  rngodm1dm2  34355  divrngcl  34380  isdrngo2  34381  mapfzcons2  38242  fnwe2lem2  38580  lmhmfgima  38613  itgpowd  38758  wnefimgd  39416  funfvima2d  39425  binomcxplemnotnn0  39511  cncmpmax  40124  mullimcf  40763  limsuppnfdlem  40841  limsupvaluz  40848  climxrrelem  40889  climxrre  40890  liminfvalxr  40923  liminflimsupxrre  40957  xlimmnfvlem2  40973  xlimpnfvlem2  40977  xlimliminflimsup  41002  cncfuni  41027  cncficcgt0  41029  cncfioobd  41038  dvsinax  41055  itgperiod  41124  fvvolioof  41133  fvvolicof  41135  stoweidlem29  41173  fourierdlem20  41271  fourierdlem53  41303  fourierdlem63  41313  fourierdlem68  41318  fourierdlem82  41332  sge0sn  41520  sge0tsms  41521  sge0cl  41522  sge0isum  41568  ismeannd  41608  hoicvr  41689  dmovn  41745  hspmbl  41770  ovolval4lem1  41790  ovnovollem1  41797  ovnovollem2  41798  issmfd  41871  issmfdf  41873  cnfsmf  41876  issmfled  41893  smfmbfcex  41895  issmfgtd  41896  smfsuplem1  41944  rmsuppss  43166  mndpsuppss  43167