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

Theorem fdm 5226
Description: The domain of a mapping. (Contributed by set.mm contributors, 2-Aug-1994.)
Assertion
Ref Expression
fdm

Proof of Theorem fdm
StepHypRef Expression
1 ffn 5223 . 2
2 fndm 5182 . 2
31, 2syl 15 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wceq 1642   cdm 4772   wfn 4776  wf 4777
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 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