Theorem fndmd 6449

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

Syntax hints:   → wi 4   = wceq 1531  dom cdm 5548   Fn wfn 6343

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 6351

This theorem is referenced by:  f1o00  6642  fvelimad  6725  offval  7408  ofrfval  7409  fsuppcurry1  30453  fsuppcurry2  30454  pfxf1  30611  s2rn  30613  s3rn  30615  cycpmfvlem  30747  cycpmfv1  30748  cycpmfv2  30749  cycpmfv3  30750  ofcfval  31350  bnj1121  32250  bnj1450  32315  frrlem4  33119  fpr2  33133  frr2  33138  diadm  38163  fnchoice  41276  wessf1ornlem  41434  limsupequzlem  41992  climrescn  42018  smflimmpt  43074  smflimsuplem7  43090