Theorem fdm 5514

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

Syntax hints:   → wi 4   = wceq 1398  dom cdm 4749   Fn wfn 5347  ⟶wf 5348

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 5355  df-f 5356

This theorem is referenced by:  fdmd  5515  fdmi  5516  fssxp  5530  ffdm  5533  dmfex  5557  f00  5559  f0dom0  5561  f0rn0  5562  foima  5595  fimadmfo  5599  foco  5601  resdif  5636  fimacnv  5806  dff3im  5822  ffvresb  5840  resflem  5841  fmptco  5843  focdmex  6308  fsuppeq  6447  fsuppeqg  6448  issmo2  6520  smoiso  6533  tfrcllemubacc  6590  rdgon  6617  frecabcl  6630  frecsuclem  6637  mapprc  6886  elpm2r  6900  map0b  6921  mapsnd  6923  mapsn  6925  brdomg  6985  pw2f1odclem  7087  fopwdom  7089  casef  7379  nn0supp  9552  frecuzrdgdomlem  10779  frecuzrdgsuctlem  10785  zfz1isolemiso  11211  ennnfonelemex  13165  intopsn  13580  iscnp3  15068  cnpnei  15084  cnntr  15090  cncnp  15095  cndis  15106  psmetdmdm  15189  xmetres  15247  metres  15248  metcnp  15377  dvcj  15574  wlkm  16334  upgr2wlkdc  16372  wlkres  16374  nninfall  16787