Theorem fndmd 6458

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 6457	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1537  dom cdm 5557   Fn wfn 6352

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 6360

This theorem is referenced by:  f1o00  6651  fvelimad  6734  offval  7418  ofrfval  7419  fsuppcurry1  30463  fsuppcurry2  30464  pfxf1  30620  s2rn  30622  s3rn  30624  cycpmfvlem  30756  cycpmfv1  30757  cycpmfv2  30758  cycpmfv3  30759  ofcfval  31359  bnj1121  32259  bnj1450  32324  frrlem4  33128  fpr2  33142  frr2  33147  diadm  38173  fnchoice  41293  wessf1ornlem  41452  limsupequzlem  42010  climrescn  42036  smflimmpt  43091  smflimsuplem7  43107