Theorem fdm 5488

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

Syntax hints:   → wi 4   = wceq 1397  dom cdm 4725   Fn wfn 5321  ⟶wf 5322

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 5329  df-f 5330

This theorem is referenced by:  fdmd  5489  fdmi  5490  fssxp  5502  ffdm  5505  dmfex  5526  f00  5528  f0dom0  5530  f0rn0  5531  foima  5564  fimadmfo  5568  foco  5570  resdif  5605  fimacnv  5776  dff3im  5792  ffvresb  5810  resflem  5811  fmptco  5813  focdmex  6277  issmo2  6455  smoiso  6468  tfrcllemubacc  6525  rdgon  6552  frecabcl  6565  frecsuclem  6572  mapprc  6821  elpm2r  6835  map0b  6856  mapsn  6859  brdomg  6919  pw2f1odclem  7020  fopwdom  7022  casef  7287  nn0supp  9454  frecuzrdgdomlem  10679  frecuzrdgsuctlem  10685  zfz1isolemiso  11103  ennnfonelemex  13036  intopsn  13451  iscnp3  14929  cnpnei  14945  cnntr  14951  cncnp  14956  cndis  14967  psmetdmdm  15050  xmetres  15108  metres  15109  metcnp  15238  dvcj  15435  wlkm  16192  upgr2wlkdc  16230  wlkres  16232  nninfall  16614