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

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

Proof of Theorem fdm
StepHypRef Expression
1 ffn 5242 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fndm 5192 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2syl 14 1 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1316  dom cdm 4509   Fn wfn 5088  wf 5089
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 5096  df-f 5097
This theorem is referenced by:  fdmd  5249  fdmi  5250  fssxp  5260  ffdm  5263  dmfex  5282  f00  5284  f0dom0  5286  f0rn0  5287  foima  5320  foco  5325  resdif  5357  fimacnv  5517  dff3im  5533  ffvresb  5551  resflem  5552  fmptco  5554  fornex  5981  issmo2  6154  smoiso  6167  tfrcllemubacc  6224  rdgon  6251  frecabcl  6264  frecsuclem  6271  mapprc  6514  elpm2r  6528  map0b  6549  mapsn  6552  brdomg  6610  fopwdom  6698  casef  6941  nn0supp  8997  frecuzrdgdomlem  10158  frecuzrdgsuctlem  10164  zfz1isolemiso  10550  ennnfonelemex  11854  iscnp3  12299  cnpnei  12315  cnntr  12321  cncnp  12326  cndis  12337  psmetdmdm  12420  xmetres  12478  metres  12479  metcnp  12608  dvcj  12769  nninfall  13131
  Copyright terms: Public domain W3C validator