New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  fdm GIF version

Theorem fdm 5226
 Description: The domain of a mapping. (Contributed by set.mm contributors, 2-Aug-1994.)
Assertion
Ref Expression
fdm (F:A–→B → dom F = A)

Proof of Theorem fdm
StepHypRef Expression
1 ffn 5223 . 2 (F:A–→BF Fn A)
2 fndm 5182 . 2 (F Fn A → dom F = A)
31, 2syl 15 1 (F:A–→B → dom F = A)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1642  dom cdm 4772   Fn wfn 4776  –→wf 4777 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177  df-an 360  df-fn 4790  df-f 4791 This theorem is referenced by:  fdmi  5227  fssxp  5232  ffdm  5234  dmfex  5247  f00  5249  foima  5274  foco  5279  f1ores  5300  f1imacnv  5302  resdif  5306  fimacnv  5411  dff3  5420  dffo4  5423  ffvresb  5431  mapprc  6004  map0b  6024  mapsn  6026  enprmaplem3  6078  enprmaplem6  6081
 Copyright terms: Public domain W3C validator