Theorem fdmd 6687

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

Syntax hints:   → wi 4   = wceq 1550  dom cdm 5636  ⟶wf 6502

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 209  df-an 399  df-fn 6509  df-f 6510

This theorem is referenced by:  fssdmd  6695  fssdm  6696  foima  6768  focnvimacdmdm  6775  resdif  6813  fssrescdmd  7093  fmptco  7096  funfvima2d  7201  focdmex  7922  suppsnop  8142  onnseq  8299  fopwdom  9042  fodomfib  9258  fodomfibOLD  9260  intrnfi  9348  ordtypelem5  9456  ordtypelem6  9457  ordtypelem7  9458  ordtypelem8  9459  brwdomn0  9503  wdomtr  9509  fseqenlem2  9967  fin23lem30  10285  isf34lem5  10321  isf34lem7  10322  isf34lem6  10323  fin1a2lem7  10349  ttukeylem6  10457  fodomb  10469  pwxpndom2  10609  hashf1lem1  14454  wrddm  14520  ccatdmss  14581  swrdcl  14645  cats1un  14720  repswswrd  14783  limsupgle  15476  limsupgre  15480  rlim  15494  rlimi  15512  lo1o1  15531  rlimuni  15549  o1co  15585  rlimcn1  15587  ruclem11  16244  1arith  16935  ramval  17016  0ram  17028  mrcuni  17625  homarcl2  18040  prfval  18203  pfxchn  18614  chnind  18625  chnccats1  18629  chnccat  18630  gsumval  18683  gsumval2  18692  mndpsuppss  18771  frmdss2  18869  ghmrn  19241  cntzmhm2  19354  gsumval3  19919  gsumzaddlem  19933  dmdprdd  20013  dprdres  20042  dprdf1  20047  dprd2da  20056  dmdprdsplit2lem  20059  dmdprdsplit2  20060  dmdprdsplit  20061  dprdsplit  20062  dpjidcl  20072  ablfac1eulem  20086  ablfac1eu  20087  ablfaclem2  20100  ablfac2  20103  lmhmlsp  21085  rhmpreimaidl  21316  frlmsslsp  21817  f1lindf  21843  mattpostpos  22483  iinopn  22931  lmbrf  23289  cnntri  23300  cnclsi  23301  lmcnp  23333  cnt0  23375  cnt1  23379  cnhaus  23383  cncmp  23421  connima  23454  1stcfb  23474  1stccnp  23491  1stckgenlem  23582  kgencn3  23587  txcnpi  23637  txcnp  23649  prdstps  23658  xkohaus  23682  xkoco2cn  23687  qtopeu  23745  hmeores  23800  fmfnfmlem2  23984  fmfnfmlem4  23986  fmfnfm  23987  lmflf  24034  txflf  24035  cnextfval  24091  cnextcn  24096  clssubg  24138  ghmcnp  24144  qustgplem  24150  tsmsval  24160  ucncn  24313  xmetdmdm  24364  metn0  24389  tmsval  24510  metustid  24583  metustexhalf  24585  metustfbas  24586  isngp2  24626  evth  24990  lmmbrf  25293  iscfil2  25297  caufval  25306  iscau2  25308  caucfil  25314  ovollb2  25520  ovolunlem1a  25527  ovoliunlem1  25533  ovoliun2  25537  ioombl1lem4  25592  uniioombllem1  25612  uniioombllem2  25614  uniioombllem6  25619  mbfconstlem  25658  ismbfcn  25660  mbfmulc2lem  25678  mbfmulc2re  25679  cncombf  25689  mbfaddlem  25691  mbflimsup  25697  i1f0rn  25713  itg1addlem5  25731  itg1climres  25745  mbfmullem2  25755  limcfval  25903  limcdif  25907  ellimc2  25908  ellimc3  25910  limccnp  25922  dvfval  25928  cpnord  25966  cpnres  25968  dvcmul  25975  dvcmulf  25976  dvexp  25984  dvgt0lem1  26033  dvcnvrelem1  26048  itgpowd  26081  plyaddlem1  26242  plymullem1  26243  plycpn  26319  aalioulem3  26364  tayl0  26391  dvntaylp  26400  ulm2  26414  ulmdvlem1  26429  xrlimcnp  26999  dchrelbas2  27267  dchrghm  27286  dchrptlem1  27294  dchrptlem2  27295  iscgrgd  28648  iscgrglt  28649  trgcgrg  28650  tgcgr4  28666  motcgrg  28679  wrdupgr  29221  wrdumgr  29233  grporndm  30648  sspn  30874  fmptcof2  32798  fnpreimac  32811  curry2ima  32850  fpwrelmap  32874  indf1ofs  32994  swrdf1  33084  pmtrcnel  33219  pmtrcnel2  33220  pmtrcnelor  33221  wrdpmtrlast  33223  cycpmcl  33246  cycpmco2f1  33254  cycpmco2rn  33255  cycpmco2lem1  33256  cycpmco2lem2  33257  cycpmco2lem3  33258  cycpmco2lem4  33259  cycpmco2lem5  33260  cycpmco2lem6  33261  cycpmco2lem7  33262  cycpmco2  33263  cyc3co2  33270  cycpmconjv  33272  fxpgaval  33297  rmfsupp2  33368  elrgspnsubrunlem2  33378  rndrhmcl  33429  elrspunidl  33560  rhmimaidl  33564  1arithidomlem2  33676  1arithidom  33677  evls1dm  33701  selvascl  33758  evlextv  33783  esplymhp  33809  esplysply  33812  esplyfval1  33814  ply1degltdimlem  33863  fldextrspunlsp  33915  irngnzply1lem  33931  irngnzply1  33932  zarcmplem  34122  rhmpreimacnlem  34125  esumpcvgval  34319  ofcfval4  34346  measdivcst  34465  oms0  34538  omsmon  34539  omssubaddlem  34540  omssubadd  34541  carsgval  34544  omsmeas  34564  sitgclg  34583  eulerpartlemgu  34618  sseqfv2  34635  rrvdm  34687  ftc2re  34839  cvmliftmolem1  35569  cvmliftlem3  35575  cvmliftlem10  35582  cvmliftlem13  35584  cvmlift2lem9  35599  cvmlift3lem6  35612  cvmlift3lem7  35613  mclsax  35857  mclsppslem  35871  mclspps  35872  fwddifval  36450  fwddifnval  36451  weiunfrlem  36762  bj-finsumval0  37715  curunc  38039  itg2addnclem2  38109  ftc1anclem5  38134  ftc1anclem6  38135  ftc1anclem8  38137  sdclem2  38179  isbnd3  38221  ssbnd  38225  bnd2lem  38228  ismtyval  38237  grpokerinj  38330  rngosn3  38361  rngodm1dm2  38369  divrngcl  38394  isdrngo2  38395  sticksstones1  42701  aks5lem2  42742  evlselvlem  43108  mapfzcons2  43238  fnwe2lem2  43566  lmhmfgima  43599  wnefimgd  44675  binomcxplemnotnn0  44870  cncmpmax  45550  mullimcf  46137  limsuppnfdlem  46213  limsupvaluz  46220  climxrrelem  46261  climxrre  46262  liminfvalxr  46295  liminflimsupxrre  46329  xlimmnfvlem2  46345  xlimpnfvlem2  46349  xlimliminflimsup  46374  cncfuni  46398  cncficcgt0  46400  cncfioobd  46409  dvsinax  46425  itgperiod  46493  fvvolioof  46501  fvvolicof  46503  stoweidlem29  46541  fourierdlem20  46639  fourierdlem53  46671  fourierdlem63  46681  fourierdlem68  46686  fourierdlem82  46700  sge0sn  46891  sge0tsms  46892  sge0cl  46893  sge0isum  46939  ismeannd  46979  hoicvr  47060  dmovn  47116  hspmbl  47141  ovolval4lem1  47161  ovnovollem1  47168  ovnovollem2  47169  issmfd  47247  issmfdf  47249  cnfsmf  47252  issmfled  47269  issmfgtd  47273  smfsuplem1  47323  smfdivdmmbl2  47353  fcores  47599  f1cof1blem  47606  f1cof1b  47609  funfocofob  47610  rmsuppss  48930  itcovalendof  49229  ffvbr  49415  lmdran  50230  cmdlan  50231