Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fndmd Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 fndmd.1 . 2 (𝜑𝐹 Fn 𝐴)
2 fndm 6448 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2syl 17 1 (𝜑 → dom 𝐹 = 𝐴)
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator