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

Theorem fdm 5246
Description: The domain of a mapping. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fdm  |-  ( F : A --> B  ->  dom  F  =  A )

Proof of Theorem fdm
StepHypRef Expression
1 ffn 5240 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fndm 5190 . 2  |-  ( F  Fn  A  ->  dom  F  =  A )
31, 2syl 14 1  |-  ( F : A --> B  ->  dom  F  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1314   dom cdm 4507    Fn wfn 5086   -->wf 5087
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106
This theorem depends on definitions:  df-bi 116  df-fn 5094  df-f 5095
This theorem is referenced by:  fdmd  5247  fdmi  5248  fssxp  5258  ffdm  5261  dmfex  5280  f00  5282  f0dom0  5284  f0rn0  5285  foima  5318  foco  5323  resdif  5355  fimacnv  5515  dff3im  5531  ffvresb  5549  resflem  5550  fmptco  5552  fornex  5979  issmo2  6152  smoiso  6165  tfrcllemubacc  6222  rdgon  6249  frecabcl  6262  frecsuclem  6269  mapprc  6512  elpm2r  6526  map0b  6547  mapsn  6550  brdomg  6608  fopwdom  6696  casef  6939  nn0supp  8980  frecuzrdgdomlem  10130  frecuzrdgsuctlem  10136  zfz1isolemiso  10522  ennnfonelemex  11822  iscnp3  12267  cnpnei  12283  cnntr  12289  cncnp  12294  cndis  12305  psmetdmdm  12388  xmetres  12446  metres  12447  metcnp  12576  dvcj  12725  nninfall  13015
  Copyright terms: Public domain W3C validator