Theorem fdm 2756

Description: The domain of a mapping.

Assertion

Ref	Expression
fdm	⊢ (F:A–→B → dom F = A)

Proof of Theorem fdm

Step	Hyp	Ref	Expression
1		ffn 2752	. 2 ⊢ (F:A–→B → F Fn A)
2		fndm 2723	. 2 ⊢ (F Fn A → dom F = A)
3	1, 2	syl 12	1 ⊢ (F:A–→B → dom F = A)

Syntax hints:   → wi 2   = wceq 1091  dom cdm 2410   Fn wfn 2417  –→wf 2418

This theorem is referenced by:  fco 2760  fssxp 2761  f00 2773  foima 2790  fornex 2793  f1ores 2813  f1imacnv 2814  f1ococnv2 2817  fopab2 2891  cbvfo 2923  mapprc 3260  map0b 3267  mapsn 3269  brdomg 3281  mapdom2lem 3388  inf3lem7 3470  fodom 3613  fodomb 3615  infmap2 4953  hoco 5598

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198  df-fn 2433  df-f 2434

metamath.org