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

Theorem fdm 5371
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 5365 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fndm 5315 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2syl 14 1 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1353  dom cdm 4626   Fn wfn 5211  wf 5212
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 5219  df-f 5220
This theorem is referenced by:  fdmd  5372  fdmi  5373  fssxp  5383  ffdm  5386  dmfex  5405  f00  5407  f0dom0  5409  f0rn0  5410  foima  5443  foco  5448  resdif  5483  fimacnv  5645  dff3im  5661  ffvresb  5679  resflem  5680  fmptco  5682  focdmex  6115  issmo2  6289  smoiso  6302  tfrcllemubacc  6359  rdgon  6386  frecabcl  6399  frecsuclem  6406  mapprc  6651  elpm2r  6665  map0b  6686  mapsn  6689  brdomg  6747  fopwdom  6835  casef  7086  nn0supp  9226  frecuzrdgdomlem  10414  frecuzrdgsuctlem  10420  zfz1isolemiso  10814  ennnfonelemex  12409  intopsn  12780  iscnp3  13634  cnpnei  13650  cnntr  13656  cncnp  13661  cndis  13672  psmetdmdm  13755  xmetres  13813  metres  13814  metcnp  13943  dvcj  14104  nninfall  14678
  Copyright terms: Public domain W3C validator