Theorem fdm 5539

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402  dom cdm 4774   Fn wfn 5372  ⟶wf 5373

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-fn 5380  df-f 5381

This theorem is used by:  fdmd  5540  fdmi  5541  fssxp  5555  ffdm  5558  dmfex  5582  f00  5584  f0dom0  5586  f0rn0  5587  foima  5620  fimadmfo  5624  foco  5626  resdif  5661  fimacnv  5837  dff3im  5853  ffvresb  5871  resflem  5872  fmptco  5874  focdmex  6344  fsuppeq  6487  fsuppeqg  6488  issmo2  6560  smoiso  6573  tfrcllemubacc  6630  rdgon  6657  frecabcl  6670  frecsuclem  6677  mapprc  6926  elpm2r  6940  map0b  6968  mapsnd  6970  mapsn  6972  brdomg  7032  pw2f1odclem  7134  fopwdom  7136  casef  7428  nn0supp  9619  frecuzrdgdomlem  10854  frecuzrdgsuctlem  10860  zfz1isolemiso  11291  ennnfonelemex  13305  intopsn  13687  iscnp3  15304  cnpnei  15320  cnntr  15326  cncnp  15331  cndis  15342  psmetdmdm  15425  xmetres  15483  metres  15484  metcnp  15613  dvcj  15810  wlkm  16580  upgr2wlkdc  16618  wlkres  16620  nninfall  17052