Theorem fndmd 6643

Description: The domain of a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypothesis

Ref	Expression
fndmd.1	⊢ (𝜑 → 𝐹 Fn 𝐴)

Assertion

Ref	Expression
fndmd	⊢ (𝜑 → dom 𝐹 = 𝐴)

Proof of Theorem fndmd

Step	Hyp	Ref	Expression
1		fndmd.1	. 2 ⊢ (𝜑 → 𝐹 Fn 𝐴)
2		fndm 6641	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5654   Fn wfn 6526

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 6534

This theorem is referenced by:  fdm  6715  f1dm  6778  f1o00  6853  fvelimad  6946  rescnvimafod  7063  f1eqcocnv  7294  ofrfvalg  7679  offval  7680  fndmexd  7900  dmmpoga  8072  fnwelem  8130  frrlem4  8288  frrlem8  8292  frrlem10  8294  fpr2  8303  fprresex  8309  wfrlem17OLD  8339  wfr2  8350  tfrlem5  8394  ixpiunwdom  9604  frr2  9774  dfac12lem1  10158  ackbij2lem3  10254  itunisuc  10433  ttukeylem3  10525  prdsbas2  17483  prdsplusgval  17487  prdsmulrval  17489  prdsleval  17491  prdsvscaval  17493  imasleval  17555  ssclem  17832  isssc  17833  rescval2  17841  issubc2  17849  cofuval  17895  resfval2  17906  resf1st  17907  resf2nd  17908  prdsmgp  20111  lspextmo  21014  dsmmfi  21698  ofco2  22389  neiss2  23039  txdis1cn  23573  qtopcld  23651  qtoprest  23655  kqsat  23669  kqdisj  23670  isr0  23675  elfm3  23888  ovolunlem1  25450  ofpreima  32643  ofpreima2  32644  fnpreimac  32649  fsuppcurry1  32702  fsuppcurry2  32703  pfxf1  32917  s2rnOLD  32919  s3rnOLD  32921  cycpmfvlem  33123  cycpmfv1  33124  cycpmfv2  33125  cycpmfv3  33126  1arithidomlem2  33551  1arithidom  33552  ply1annidllem  33735  ofcfval  34129  probfinmeasb  34460  bnj564  34775  bnj1121  35016  bnj1442  35080  bnj1450  35081  bnj1501  35098  fnrelpredd  35120  sdclem2  37766  prdstotbnd  37818  diadm  41054  dibdiadm  41174  dibdmN  41176  dicdmN  41203  dihdm  41288  aks4d1p1p5  42088  aks6d1c6lem2  42184  tfsconcat0b  43370  fnchoice  45053  wessf1ornlem  45209  limsupequzlem  45751  climrescn  45777  icccncfext  45916  stoweidlem35  46064  stoweidlem59  46088  smflimmpt  46839  smflimsuplem7  46855  iinfssclem1  49021  infsubc2d  49029  oppfvallem  49081  funcoppc3  49090  uptposlem  49130