Theorem fdmd 6731

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

Syntax hints:   → wi 4   = wceq 1533  dom cdm 5677  ⟶wf 6543

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 395  df-fn 6550  df-f 6551

This theorem is referenced by:  fssdmd  6739  fssdm  6740  foima  6813  focnvimacdmdm  6820  resdif  6857  fssrescdmd  7133  fmptco  7136  funfvima2d  7242  focdmex  7958  suppsnop  8181  onnseq  8363  fopwdom  9103  fodomfib  9350  intrnfi  9439  ordtypelem5  9545  ordtypelem6  9546  ordtypelem7  9547  ordtypelem8  9548  brwdomn0  9592  wdomtr  9598  fseqenlem2  10048  fin23lem30  10365  isf34lem5  10401  isf34lem7  10402  isf34lem6  10403  fin1a2lem7  10429  ttukeylem6  10537  fodomb  10549  pwxpndom2  10688  hashf1lem1  14447  hashf1lem1OLD  14448  wrddm  14503  swrdcl  14627  cats1un  14703  repswswrd  14766  limsupgle  15453  limsupgre  15457  rlim  15471  rlimi  15489  lo1o1  15508  rlimuni  15526  o1co  15562  rlimcn1  15564  ruclem11  16216  1arith  16895  ramval  16976  0ram  16988  mrcuni  17600  homarcl2  18023  prfval  18189  gsumval  18636  gsumval2  18645  frmdss2  18819  ghmrn  19187  cntzmhm2  19297  gsumval3  19866  gsumzaddlem  19880  dmdprdd  19960  dprdres  19989  dprdf1  19994  dprd2da  20003  dmdprdsplit2lem  20006  dmdprdsplit2  20007  dmdprdsplit  20008  dprdsplit  20009  dpjidcl  20019  ablfac1eulem  20033  ablfac1eu  20034  ablfaclem2  20047  ablfac2  20050  lmhmlsp  20938  frlmsslsp  21734  f1lindf  21760  mattpostpos  22386  iinopn  22834  lmbrf  23194  cnntri  23205  cnclsi  23206  lmcnp  23238  cnt0  23280  cnt1  23284  cnhaus  23288  cncmp  23326  connima  23359  1stcfb  23379  1stccnp  23396  1stckgenlem  23487  kgencn3  23492  txcnpi  23542  txcnp  23554  prdstps  23563  xkohaus  23587  xkoco2cn  23592  qtopeu  23650  hmeores  23705  fmfnfmlem2  23889  fmfnfmlem4  23891  fmfnfm  23892  lmflf  23939  txflf  23940  cnextfval  23996  cnextcn  24001  clssubg  24043  ghmcnp  24049  qustgplem  24055  tsmsval  24065  ucncn  24220  xmetdmdm  24271  metn0  24296  tmsval  24419  metustid  24493  metustexhalf  24495  metustfbas  24496  isngp2  24536  evth  24915  lmmbrf  25220  iscfil2  25224  caufval  25233  iscau2  25235  caucfil  25241  ovollb2  25448  ovolunlem1a  25455  ovoliunlem1  25461  ovoliun2  25465  ioombl1lem4  25520  uniioombllem1  25540  uniioombllem2  25542  uniioombllem6  25547  mbfconstlem  25586  ismbfcn  25588  mbfmulc2lem  25606  mbfmulc2re  25607  cncombf  25617  mbfaddlem  25619  mbflimsup  25625  i1f0rn  25641  itg1addlem5  25660  itg1climres  25674  mbfmullem2  25684  limcfval  25831  limcdif  25835  ellimc2  25836  ellimc3  25838  limccnp  25850  dvfval  25856  cpnord  25895  cpnres  25897  dvcmul  25905  dvcmulf  25906  dvexp  25915  dvgt0lem1  25965  dvcnvrelem1  25980  itgpowd  26015  plyaddlem1  26177  plymullem1  26178  plycpn  26254  aalioulem3  26299  tayl0  26326  dvntaylp  26336  ulm2  26351  ulmdvlem1  26366  xrlimcnp  26930  dchrelbas2  27200  dchrghm  27219  dchrptlem1  27227  dchrptlem2  27228  iscgrgd  28373  iscgrglt  28374  trgcgrg  28375  tgcgr4  28391  motcgrg  28404  wrdupgr  28954  wrdumgr  28966  grporndm  30376  sspn  30602  fmptcof2  32500  fnpreimac  32514  curry2ima  32545  fpwrelmap  32572  swrdf1  32734  pmtrcnel  32869  pmtrcnel2  32870  pmtrcnelor  32871  cycpmcl  32894  cycpmco2f1  32902  cycpmco2rn  32903  cycpmco2lem1  32904  cycpmco2lem2  32905  cycpmco2lem3  32906  cycpmco2lem4  32907  cycpmco2lem5  32908  cycpmco2lem6  32909  cycpmco2lem7  32910  cycpmco2  32911  cyc3co2  32918  cycpmconjv  32920  rmfsupp2  33002  rndrhmcl  33045  rhmpreimaidl  33195  elrspunidl  33206  rhmimaidl  33210  evls1dm  33319  ply1degltdimlem  33390  irngnzply1lem  33438  irngnzply1  33439  zarcmplem  33552  rhmpreimacnlem  33555  indf1ofs  33715  esumpcvgval  33767  ofcfval4  33794  measdivcst  33913  oms0  33987  omsmon  33988  omssubaddlem  33989  omssubadd  33990  carsgval  33993  omsmeas  34013  sitgclg  34032  eulerpartlemgu  34067  sseqfv2  34084  rrvdm  34136  ftc2re  34300  cvmliftmolem1  34961  cvmliftlem3  34967  cvmliftlem10  34974  cvmliftlem13  34976  cvmlift2lem9  34991  cvmlift3lem6  35004  cvmlift3lem7  35005  mclsax  35249  mclsppslem  35263  mclspps  35264  fwddifval  35828  fwddifnval  35829  bj-finsumval0  36834  curunc  37145  itg2addnclem2  37215  ftc1anclem5  37240  ftc1anclem6  37241  ftc1anclem8  37243  sdclem2  37285  isbnd3  37327  ssbnd  37331  bnd2lem  37334  ismtyval  37343  grpokerinj  37436  rngosn3  37467  rngodm1dm2  37475  divrngcl  37500  isdrngo2  37501  sticksstones1  41687  evlselvlem  41884  mapfzcons2  42204  fnwe2lem2  42540  lmhmfgima  42573  wnefimgd  43656  binomcxplemnotnn0  43858  cncmpmax  44459  mullimcf  45074  limsuppnfdlem  45152  limsupvaluz  45159  climxrrelem  45200  climxrre  45201  liminfvalxr  45234  liminflimsupxrre  45268  xlimmnfvlem2  45284  xlimpnfvlem2  45288  xlimliminflimsup  45313  cncfuni  45337  cncficcgt0  45339  cncfioobd  45348  dvsinax  45364  itgperiod  45432  fvvolioof  45440  fvvolicof  45442  stoweidlem29  45480  fourierdlem20  45578  fourierdlem53  45610  fourierdlem63  45620  fourierdlem68  45625  fourierdlem82  45639  sge0sn  45830  sge0tsms  45831  sge0cl  45832  sge0isum  45878  ismeannd  45918  hoicvr  45999  dmovn  46055  hspmbl  46080  ovolval4lem1  46100  ovnovollem1  46107  ovnovollem2  46108  issmfd  46186  issmfdf  46188  cnfsmf  46191  issmfled  46208  issmfgtd  46212  smfsuplem1  46262  smfdivdmmbl2  46292  fcores  46512  f1cof1blem  46519  f1cof1b  46520  funfocofob  46521  rmsuppss  47546  mndpsuppss  47547  itcovalendof  47854