Theorem fdm 3631

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

Syntax hints:   -> wi 3   = wceq 956  dom cdm 3170   Fn wfn 3177  -->wf 3178

This theorem is referenced by:  fdmi 3632  fco 3636  fssxp 3637  ffdm 3639  dmfex 3655  f00 3657  foima 3676  fornex 3679  foco 3682  f1ores 3703  f1imacnv 3705  f1ococnv2 3708  fimacnv 3810  dff2 3817  fopab2 3823  cbvfo 3885  mapprc 4326  map0b 4343  mapsn 4345  brdomg 4376  fodomr 4483  mapdom2lem 4493  fodomfiOLD 4566  fodomfibOLD 4567  inf3lem7 4619  fodom 4798  fodomb 4800  fseqsupcl 6525  fseqsupub 6526  infmap2 7581  iscnp2 7761  cnpco 7769  iscncl 7770  cnsscnp 7772  cncnplem4 7777  cnconst 7780  ismet 7798  dfms2 7799  metssba 7809  metne0 7821  metreslem 7822  metres 7823  metcnplem 7886  metcnp 7887  metcnp3 7896  metcnss 7898  metcnss2 7899  grprndm 8054  resgrprn 8095  subgres 8117  vcoprne 8198  nvdm 8289  imsdval 8317  imsba 8321  ipfval 8352  sspn 8395  dmadjrnb 9830  ghomfo 10391  mapdiscn 10511  dcsda 10666

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-fn 3193  df-f 3194

Copyright terms: Public domain