Theorem fdm 5373

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

Syntax hints:   → wi 4   = wceq 1353  dom cdm 4628   Fn wfn 5213  ⟶wf 5214

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 5221  df-f 5222

This theorem is referenced by:  fdmd  5374  fdmi  5375  fssxp  5385  ffdm  5388  dmfex  5407  f00  5409  f0dom0  5411  f0rn0  5412  foima  5445  foco  5450  resdif  5485  fimacnv  5647  dff3im  5663  ffvresb  5681  resflem  5682  fmptco  5684  focdmex  6118  issmo2  6292  smoiso  6305  tfrcllemubacc  6362  rdgon  6389  frecabcl  6402  frecsuclem  6409  mapprc  6654  elpm2r  6668  map0b  6689  mapsn  6692  brdomg  6750  fopwdom  6838  casef  7089  nn0supp  9230  frecuzrdgdomlem  10419  frecuzrdgsuctlem  10425  zfz1isolemiso  10821  ennnfonelemex  12417  intopsn  12791  iscnp3  13788  cnpnei  13804  cnntr  13810  cncnp  13815  cndis  13826  psmetdmdm  13909  xmetres  13967  metres  13968  metcnp  14097  dvcj  14258  nninfall  14843