Theorem fdm 5409

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 5403	. 2 |- ( F : A --> B -> F Fn A )
2		fndm 5353	. 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 4659   Fn wfn 5249   -->wf 5250

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 5257  df-f 5258

This theorem is referenced by:  fdmd  5410  fdmi  5411  fssxp  5421  ffdm  5424  dmfex  5443  f00  5445  f0dom0  5447  f0rn0  5448  foima  5481  fimadmfo  5485  foco  5487  resdif  5522  fimacnv  5687  dff3im  5703  ffvresb  5721  resflem  5722  fmptco  5724  focdmex  6167  issmo2  6342  smoiso  6355  tfrcllemubacc  6412  rdgon  6439  frecabcl  6452  frecsuclem  6459  mapprc  6706  elpm2r  6720  map0b  6741  mapsn  6744  brdomg  6802  pw2f1odclem  6890  fopwdom  6892  casef  7147  nn0supp  9292  frecuzrdgdomlem  10488  frecuzrdgsuctlem  10494  zfz1isolemiso  10910  ennnfonelemex  12571  intopsn  12950  iscnp3  14371  cnpnei  14387  cnntr  14393  cncnp  14398  cndis  14409  psmetdmdm  14492  xmetres  14550  metres  14551  metcnp  14680  dvcj  14858  nninfall  15499