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

Theorem fdm 5287
 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 5281 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fndm 5231 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2syl 14 1 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1332  dom cdm 4548   Fn wfn 5127  ⟶wf 5128 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 5135  df-f 5136 This theorem is referenced by:  fdmd  5288  fdmi  5289  fssxp  5299  ffdm  5302  dmfex  5321  f00  5323  f0dom0  5325  f0rn0  5326  foima  5359  foco  5364  resdif  5398  fimacnv  5558  dff3im  5574  ffvresb  5592  resflem  5593  fmptco  5595  fornex  6022  issmo2  6195  smoiso  6208  tfrcllemubacc  6265  rdgon  6292  frecabcl  6305  frecsuclem  6312  mapprc  6555  elpm2r  6569  map0b  6590  mapsn  6593  brdomg  6651  fopwdom  6739  casef  6983  nn0supp  9073  frecuzrdgdomlem  10241  frecuzrdgsuctlem  10247  zfz1isolemiso  10634  ennnfonelemex  11983  iscnp3  12431  cnpnei  12447  cnntr  12453  cncnp  12458  cndis  12469  psmetdmdm  12552  xmetres  12610  metres  12611  metcnp  12740  dvcj  12901  nninfall  13398
 Copyright terms: Public domain W3C validator