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

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

Proof of Theorem fdm
StepHypRef Expression
1 ffn 4989 . 2 (𝐹:AB𝐹 Fn A)
2 fndm 4941 . 2 (𝐹 Fn A → dom 𝐹 = A)
31, 2syl 14 1 (𝐹:AB → dom 𝐹 = A)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1242  dom cdm 4288   Fn wfn 4840  wf 4841
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100
This theorem depends on definitions:  df-bi 110  df-fn 4848  df-f 4849
This theorem is referenced by:  fdmi  4994  fssxp  5001  ffdm  5004  dmfex  5022  f00  5024  foima  5054  foco  5059  resdif  5091  fimacnv  5239  dff3im  5255  ffvresb  5271  fmptco  5273  fornex  5684  issmo2  5845  smoiso  5858  brdomg  6165  fopwdom  6246  nn0supp  8010
  Copyright terms: Public domain W3C validator