Theorem fdmd 6673

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5625  ⟶wf 6489

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 6496  df-f 6497

This theorem is referenced by:  fssdmd  6681  fssdm  6682  foima  6752  focnvimacdmdm  6759  resdif  6796  fssrescdmd  7073  fmptco  7076  funfvima2d  7180  focdmex  7902  suppsnop  8122  onnseq  8278  fopwdom  9017  fodomfib  9233  fodomfibOLD  9235  intrnfi  9323  ordtypelem5  9431  ordtypelem6  9432  ordtypelem7  9433  ordtypelem8  9434  brwdomn0  9478  wdomtr  9484  fseqenlem2  9939  fin23lem30  10256  isf34lem5  10292  isf34lem7  10293  isf34lem6  10294  fin1a2lem7  10320  ttukeylem6  10428  fodomb  10440  pwxpndom2  10580  hashf1lem1  14382  wrddm  14448  ccatdmss  14509  swrdcl  14573  cats1un  14648  repswswrd  14711  limsupgle  15404  limsupgre  15408  rlim  15422  rlimi  15440  lo1o1  15459  rlimuni  15477  o1co  15513  rlimcn1  15515  ruclem11  16169  1arith  16859  ramval  16940  0ram  16952  mrcuni  17548  homarcl2  17963  prfval  18126  pfxchn  18537  chnind  18548  chnccats1  18552  chnccat  18553  gsumval  18606  gsumval2  18615  mndpsuppss  18694  frmdss2  18792  ghmrn  19162  cntzmhm2  19275  gsumval3  19840  gsumzaddlem  19854  dmdprdd  19934  dprdres  19963  dprdf1  19968  dprd2da  19977  dmdprdsplit2lem  19980  dmdprdsplit2  19981  dmdprdsplit  19982  dprdsplit  19983  dpjidcl  19993  ablfac1eulem  20007  ablfac1eu  20008  ablfaclem2  20021  ablfac2  20024  lmhmlsp  21005  rhmpreimaidl  21236  frlmsslsp  21755  f1lindf  21781  mattpostpos  22402  iinopn  22850  lmbrf  23208  cnntri  23219  cnclsi  23220  lmcnp  23252  cnt0  23294  cnt1  23298  cnhaus  23302  cncmp  23340  connima  23373  1stcfb  23393  1stccnp  23410  1stckgenlem  23501  kgencn3  23506  txcnpi  23556  txcnp  23568  prdstps  23577  xkohaus  23601  xkoco2cn  23606  qtopeu  23664  hmeores  23719  fmfnfmlem2  23903  fmfnfmlem4  23905  fmfnfm  23906  lmflf  23953  txflf  23954  cnextfval  24010  cnextcn  24015  clssubg  24057  ghmcnp  24063  qustgplem  24069  tsmsval  24079  ucncn  24232  xmetdmdm  24283  metn0  24308  tmsval  24429  metustid  24502  metustexhalf  24504  metustfbas  24505  isngp2  24545  evth  24918  lmmbrf  25222  iscfil2  25226  caufval  25235  iscau2  25237  caucfil  25243  ovollb2  25450  ovolunlem1a  25457  ovoliunlem1  25463  ovoliun2  25467  ioombl1lem4  25522  uniioombllem1  25542  uniioombllem2  25544  uniioombllem6  25549  mbfconstlem  25588  ismbfcn  25590  mbfmulc2lem  25608  mbfmulc2re  25609  cncombf  25619  mbfaddlem  25621  mbflimsup  25627  i1f0rn  25643  itg1addlem5  25661  itg1climres  25675  mbfmullem2  25685  limcfval  25833  limcdif  25837  ellimc2  25838  ellimc3  25840  limccnp  25852  dvfval  25858  cpnord  25897  cpnres  25899  dvcmul  25907  dvcmulf  25908  dvexp  25917  dvgt0lem1  25967  dvcnvrelem1  25982  itgpowd  26017  plyaddlem1  26178  plymullem1  26179  plycpn  26257  aalioulem3  26302  tayl0  26329  dvntaylp  26339  ulm2  26354  ulmdvlem1  26369  xrlimcnp  26938  dchrelbas2  27208  dchrghm  27227  dchrptlem1  27235  dchrptlem2  27236  iscgrgd  28568  iscgrglt  28569  trgcgrg  28570  tgcgr4  28586  motcgrg  28599  wrdupgr  29141  wrdumgr  29153  grporndm  30568  sspn  30794  fmptcof2  32717  fnpreimac  32730  curry2ima  32769  fpwrelmap  32793  indf1ofs  32929  swrdf1  33019  pmtrcnel  33152  pmtrcnel2  33153  pmtrcnelor  33154  wrdpmtrlast  33156  cycpmcl  33179  cycpmco2f1  33187  cycpmco2rn  33188  cycpmco2lem1  33189  cycpmco2lem2  33190  cycpmco2lem3  33191  cycpmco2lem4  33192  cycpmco2lem5  33193  cycpmco2lem6  33194  cycpmco2lem7  33195  cycpmco2  33196  cyc3co2  33203  cycpmconjv  33205  fxpgaval  33230  rmfsupp2  33301  elrgspnsubrunlem2  33311  rndrhmcl  33359  elrspunidl  33490  rhmimaidl  33494  1arithidomlem2  33598  1arithidom  33599  evls1dm  33623  evlextv  33688  esplymhp  33707  esplysply  33710  ply1degltdimlem  33760  fldextrspunlsp  33812  irngnzply1lem  33828  irngnzply1  33829  zarcmplem  34019  rhmpreimacnlem  34022  esumpcvgval  34216  ofcfval4  34243  measdivcst  34362  oms0  34435  omsmon  34436  omssubaddlem  34437  omssubadd  34438  carsgval  34441  omsmeas  34461  sitgclg  34480  eulerpartlemgu  34515  sseqfv2  34532  rrvdm  34584  ftc2re  34736  cvmliftmolem1  35456  cvmliftlem3  35462  cvmliftlem10  35469  cvmliftlem13  35471  cvmlift2lem9  35486  cvmlift3lem6  35499  cvmlift3lem7  35500  mclsax  35744  mclsppslem  35758  mclspps  35759  fwddifval  36337  fwddifnval  36338  weiunfrlem  36639  bj-finsumval0  37461  curunc  37774  itg2addnclem2  37844  ftc1anclem5  37869  ftc1anclem6  37870  ftc1anclem8  37872  sdclem2  37914  isbnd3  37956  ssbnd  37960  bnd2lem  37963  ismtyval  37972  grpokerinj  38065  rngosn3  38096  rngodm1dm2  38104  divrngcl  38129  isdrngo2  38130  sticksstones1  42437  aks5lem2  42478  evlselvlem  42865  mapfzcons2  42997  fnwe2lem2  43329  lmhmfgima  43362  wnefimgd  44438  binomcxplemnotnn0  44633  cncmpmax  45313  mullimcf  45905  limsuppnfdlem  45981  limsupvaluz  45988  climxrrelem  46029  climxrre  46030  liminfvalxr  46063  liminflimsupxrre  46097  xlimmnfvlem2  46113  xlimpnfvlem2  46117  xlimliminflimsup  46142  cncfuni  46166  cncficcgt0  46168  cncfioobd  46177  dvsinax  46193  itgperiod  46261  fvvolioof  46269  fvvolicof  46271  stoweidlem29  46309  fourierdlem20  46407  fourierdlem53  46439  fourierdlem63  46449  fourierdlem68  46454  fourierdlem82  46468  sge0sn  46659  sge0tsms  46660  sge0cl  46661  sge0isum  46707  ismeannd  46747  hoicvr  46828  dmovn  46884  hspmbl  46909  ovolval4lem1  46929  ovnovollem1  46936  ovnovollem2  46937  issmfd  47015  issmfdf  47017  cnfsmf  47020  issmfled  47037  issmfgtd  47041  smfsuplem1  47091  smfdivdmmbl2  47121  fcores  47349  f1cof1blem  47356  f1cof1b  47359  funfocofob  47360  rmsuppss  48652  itcovalendof  48951  ffvbr  49137  lmdran  49952  cmdlan  49953