ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fdm GIF version

Theorem fdm 5078
Description: The domain of a mapping. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fdm (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)

Proof of Theorem fdm
StepHypRef Expression
1 ffn 5074 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fndm 5026 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2syl 14 1 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1259  dom cdm 4373   Fn wfn 4925  wf 4926
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104
This theorem depends on definitions:  df-bi 114  df-fn 4933  df-f 4934
This theorem is referenced by:  fdmi  5079  fssxp  5086  ffdm  5089  dmfex  5107  f00  5109  foima  5139  foco  5144  resdif  5176  fimacnv  5324  dff3im  5340  ffvresb  5356  fmptco  5358  fornex  5770  issmo2  5935  smoiso  5948  brdomg  6260  fopwdom  6341  nn0supp  8291
  Copyright terms: Public domain W3C validator