Theorem fdm 5414

Description: The domain of a mapping. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
fdm	|- ( F : A --> B -> dom F = A )

Proof of Theorem fdm

Step	Hyp	Ref	Expression
1		ffn 5408	. 2 |- ( F : A --> B -> F Fn A )
2		fndm 5358	. 2 |- ( F Fn A -> dom F = A )
3	1, 2	syl 14	1 |- ( F : A --> B -> dom F = A )

Syntax hints:   -> wi 4   = wceq 1364   dom cdm 4664   Fn wfn 5254   -->wf 5255

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 5262  df-f 5263

This theorem is referenced by:  fdmd  5415  fdmi  5416  fssxp  5426  ffdm  5429  dmfex  5448  f00  5450  f0dom0  5452  f0rn0  5453  foima  5486  fimadmfo  5490  foco  5492  resdif  5527  fimacnv  5692  dff3im  5708  ffvresb  5726  resflem  5727  fmptco  5729  focdmex  6173  issmo2  6348  smoiso  6361  tfrcllemubacc  6418  rdgon  6445  frecabcl  6458  frecsuclem  6465  mapprc  6712  elpm2r  6726  map0b  6747  mapsn  6750  brdomg  6808  pw2f1odclem  6896  fopwdom  6898  casef  7155  nn0supp  9303  frecuzrdgdomlem  10511  frecuzrdgsuctlem  10517  zfz1isolemiso  10933  ennnfonelemex  12641  intopsn  13020  iscnp3  14449  cnpnei  14465  cnntr  14471  cncnp  14476  cndis  14487  psmetdmdm  14570  xmetres  14628  metres  14629  metcnp  14758  dvcj  14955  nninfall  15663