Theorem fdm 5485

Description: The domain of a mapping. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
fdm	⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)

Proof of Theorem fdm

Step	Hyp	Ref	Expression
1		ffn 5479	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fndm 5426	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1395  dom cdm 4723   Fn wfn 5319  ⟶wf 5320

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 5327  df-f 5328

This theorem is referenced by:  fdmd  5486  fdmi  5487  fssxp  5499  ffdm  5502  dmfex  5523  f00  5525  f0dom0  5527  f0rn0  5528  foima  5561  fimadmfo  5565  foco  5567  resdif  5602  fimacnv  5772  dff3im  5788  ffvresb  5806  resflem  5807  fmptco  5809  focdmex  6272  issmo2  6450  smoiso  6463  tfrcllemubacc  6520  rdgon  6547  frecabcl  6560  frecsuclem  6567  mapprc  6816  elpm2r  6830  map0b  6851  mapsn  6854  brdomg  6914  pw2f1odclem  7015  fopwdom  7017  casef  7278  nn0supp  9444  frecuzrdgdomlem  10669  frecuzrdgsuctlem  10675  zfz1isolemiso  11093  ennnfonelemex  13025  intopsn  13440  iscnp3  14917  cnpnei  14933  cnntr  14939  cncnp  14944  cndis  14955  psmetdmdm  15038  xmetres  15096  metres  15097  metcnp  15226  dvcj  15423  wlkm  16136  upgr2wlkdc  16172  wlkres  16174  nninfall  16547