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  6276  issmo2  6454  smoiso  6467  tfrcllemubacc  6524  rdgon  6551  frecabcl  6564  frecsuclem  6571  mapprc  6820  elpm2r  6834  map0b  6855  mapsn  6858  brdomg  6918  pw2f1odclem  7019  fopwdom  7021  casef  7286  nn0supp  9453  frecuzrdgdomlem  10678  frecuzrdgsuctlem  10684  zfz1isolemiso  11102  ennnfonelemex  13034  intopsn  13449  iscnp3  14926  cnpnei  14942  cnntr  14948  cncnp  14953  cndis  14964  psmetdmdm  15047  xmetres  15105  metres  15106  metcnp  15235  dvcj  15432  wlkm  16189  upgr2wlkdc  16227  wlkres  16229  nninfall  16611