Theorem fdm 5542

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402  dom cdm 4776   Fn wfn 5375  ⟶wf 5376

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 5383  df-f 5384

This theorem is used by:  fdmd  5543  fdmi  5544  fssxp  5558  ffdm  5561  dmfex  5585  f00  5587  f0dom0  5589  f0rn0  5590  foima  5623  fimadmfo  5627  foco  5629  resdif  5664  fimacnv  5840  dff3im  5856  ffvresb  5874  resflem  5875  fmptco  5877  focdmex  6348  fsuppeq  6491  fsuppeqg  6492  issmo2  6565  smoiso  6578  tfrcllemubacc  6635  rdgon  6662  frecabcl  6675  frecsuclem  6682  mapprc  6931  elpm2r  6945  map0b  6973  mapsnd  6976  mapsn  6978  brdomg  7038  pw2f1odclem  7140  fopwdom  7142  casef  7434  nn0supp  9628  frecuzrdgdomlem  10874  frecuzrdgsuctlem  10880  zfz1isolemiso  11312  ennnfonelemex  13362  intopsn  13745  iscnp3  15446  cnpnei  15462  cnntr  15468  cncnp  15473  cndis  15484  psmetdmdm  15567  xmetres  15625  metres  15626  metcnp  15755  dvcj  15952  wlkm  16802  upgr2wlkdc  16840  wlkres  16842  nninfall  17275