Theorem fdm 5236

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

Syntax hints:   → wi 4   = wceq 1314  dom cdm 4499   Fn wfn 5076  ⟶wf 5077

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-fn 5084  df-f 5085

This theorem is referenced by:  fdmd  5237  fdmi  5238  fssxp  5248  ffdm  5251  dmfex  5270  f00  5272  f0dom0  5274  f0rn0  5275  foima  5308  foco  5313  resdif  5345  fimacnv  5503  dff3im  5519  ffvresb  5537  resflem  5538  fmptco  5540  fornex  5967  issmo2  6140  smoiso  6153  tfrcllemubacc  6210  rdgon  6237  frecabcl  6250  frecsuclem  6257  mapprc  6500  elpm2r  6514  map0b  6535  mapsn  6538  brdomg  6596  fopwdom  6683  casef  6925  nn0supp  8933  frecuzrdgdomlem  10083  frecuzrdgsuctlem  10089  zfz1isolemiso  10475  ennnfonelemex  11772  iscnp3  12214  cnpnei  12230  cnntr  12236  cncnp  12241  cndis  12252  psmetdmdm  12313  xmetres  12371  metres  12372  metcnp  12501  nninfall  12896