Theorem fdm 5353

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

Syntax hints:   → wi 4   = wceq 1348  dom cdm 4611   Fn wfn 5193  ⟶wf 5194

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

This theorem depends on definitions:  df-bi 116  df-fn 5201  df-f 5202

This theorem is referenced by:  fdmd  5354  fdmi  5355  fssxp  5365  ffdm  5368  dmfex  5387  f00  5389  f0dom0  5391  f0rn0  5392  foima  5425  foco  5430  resdif  5464  fimacnv  5625  dff3im  5641  ffvresb  5659  resflem  5660  fmptco  5662  fornex  6094  issmo2  6268  smoiso  6281  tfrcllemubacc  6338  rdgon  6365  frecabcl  6378  frecsuclem  6385  mapprc  6630  elpm2r  6644  map0b  6665  mapsn  6668  brdomg  6726  fopwdom  6814  casef  7065  nn0supp  9187  frecuzrdgdomlem  10373  frecuzrdgsuctlem  10379  zfz1isolemiso  10774  ennnfonelemex  12369  intopsn  12621  iscnp3  12997  cnpnei  13013  cnntr  13019  cncnp  13024  cndis  13035  psmetdmdm  13118  xmetres  13176  metres  13177  metcnp  13306  dvcj  13467  nninfall  14042