Theorem fdm 5479

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 5473	. 2 |- ( F : A --> B -> F Fn A )
2		fndm 5420	. 2 |- ( F Fn A -> dom F = A )
3	1, 2	syl 14	1 |- ( F : A --> B -> dom F = A )

Syntax hints:   -> wi 4   = wceq 1395   dom cdm 4719   Fn wfn 5313   -->wf 5314

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 5321  df-f 5322

This theorem is referenced by:  fdmd  5480  fdmi  5481  fssxp  5491  ffdm  5494  dmfex  5515  f00  5517  f0dom0  5519  f0rn0  5520  foima  5553  fimadmfo  5557  foco  5559  resdif  5594  fimacnv  5764  dff3im  5780  ffvresb  5798  resflem  5799  fmptco  5801  focdmex  6260  issmo2  6435  smoiso  6448  tfrcllemubacc  6505  rdgon  6532  frecabcl  6545  frecsuclem  6552  mapprc  6799  elpm2r  6813  map0b  6834  mapsn  6837  brdomg  6897  pw2f1odclem  6995  fopwdom  6997  casef  7255  nn0supp  9421  frecuzrdgdomlem  10639  frecuzrdgsuctlem  10645  zfz1isolemiso  11061  ennnfonelemex  12985  intopsn  13400  iscnp3  14877  cnpnei  14893  cnntr  14899  cncnp  14904  cndis  14915  psmetdmdm  14998  xmetres  15056  metres  15057  metcnp  15186  dvcj  15383  wlkm  16051  nninfall  16375