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

Theorem fdm 5387
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 5381 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fndm 5331 . 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 1364   dom cdm 4641    Fn wfn 5227   -->wf 5228
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107
This theorem depends on definitions:  df-bi 117  df-fn 5235  df-f 5236
This theorem is referenced by:  fdmd  5388  fdmi  5389  fssxp  5399  ffdm  5402  dmfex  5421  f00  5423  f0dom0  5425  f0rn0  5426  foima  5459  foco  5464  resdif  5499  fimacnv  5662  dff3im  5678  ffvresb  5696  resflem  5697  fmptco  5699  focdmex  6135  issmo2  6309  smoiso  6322  tfrcllemubacc  6379  rdgon  6406  frecabcl  6419  frecsuclem  6426  mapprc  6673  elpm2r  6687  map0b  6708  mapsn  6711  brdomg  6769  pw2f1odclem  6857  fopwdom  6859  casef  7112  nn0supp  9253  frecuzrdgdomlem  10443  frecuzrdgsuctlem  10449  zfz1isolemiso  10846  ennnfonelemex  12460  intopsn  12836  iscnp3  14140  cnpnei  14156  cnntr  14162  cncnp  14167  cndis  14178  psmetdmdm  14261  xmetres  14319  metres  14320  metcnp  14449  dvcj  14610  nninfall  15196
  Copyright terms: Public domain W3C validator