Theorem fdm 5495

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 5489	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fndm 5436	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1398  dom cdm 4731   Fn wfn 5328  ⟶wf 5329

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 5336  df-f 5337

This theorem is referenced by:  fdmd  5496  fdmi  5497  fssxp  5510  ffdm  5513  dmfex  5535  f00  5537  f0dom0  5539  f0rn0  5540  foima  5573  fimadmfo  5577  foco  5579  resdif  5614  fimacnv  5784  dff3im  5800  ffvresb  5818  resflem  5819  fmptco  5821  focdmex  6286  fsuppeq  6425  fsuppeqg  6426  issmo2  6498  smoiso  6511  tfrcllemubacc  6568  rdgon  6595  frecabcl  6608  frecsuclem  6615  mapprc  6864  elpm2r  6878  map0b  6899  mapsn  6902  brdomg  6962  pw2f1odclem  7063  fopwdom  7065  casef  7330  nn0supp  9498  frecuzrdgdomlem  10725  frecuzrdgsuctlem  10731  zfz1isolemiso  11149  ennnfonelemex  13098  intopsn  13513  iscnp3  14997  cnpnei  15013  cnntr  15019  cncnp  15024  cndis  15035  psmetdmdm  15118  xmetres  15176  metres  15177  metcnp  15306  dvcj  15503  wlkm  16263  upgr2wlkdc  16301  wlkres  16303  nninfall  16718