Theorem fdm 5519

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

Syntax hints:   → wi 4   = wceq 1398  dom cdm 4754   Fn wfn 5352  ⟶wf 5353

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 5360  df-f 5361

This theorem is referenced by:  fdmd  5520  fdmi  5521  fssxp  5535  ffdm  5538  dmfex  5562  f00  5564  f0dom0  5566  f0rn0  5567  foima  5600  fimadmfo  5604  foco  5606  resdif  5641  fimacnv  5811  dff3im  5827  ffvresb  5845  resflem  5846  fmptco  5848  focdmex  6317  fsuppeq  6460  fsuppeqg  6461  issmo2  6533  smoiso  6546  tfrcllemubacc  6603  rdgon  6630  frecabcl  6643  frecsuclem  6650  mapprc  6899  elpm2r  6913  map0b  6934  mapsnd  6936  mapsn  6938  brdomg  6998  pw2f1odclem  7100  fopwdom  7102  casef  7392  nn0supp  9569  frecuzrdgdomlem  10803  frecuzrdgsuctlem  10809  zfz1isolemiso  11236  ennnfonelemex  13249  intopsn  13630  iscnp3  15194  cnpnei  15210  cnntr  15216  cncnp  15221  cndis  15232  psmetdmdm  15315  xmetres  15373  metres  15374  metcnp  15503  dvcj  15700  wlkm  16460  upgr2wlkdc  16498  wlkres  16500  nninfall  16913