Theorem fdm 3629

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 3625	. 2 |- (F:A-->B -> F Fn A)
2		fndm 3585	. 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 3168   Fn wfn 3175  -->wf 3176

This theorem is referenced by:  fdmi 3630  fco 3634  fssxp 3635  ffdm 3637  dmfex 3653  f00 3655  foima 3674  fornex 3677  foco 3680  f1ores 3701  f1imacnv 3703  f1ococnv2 3706  fimacnv 3808  dff2 3815  fopab2 3821  cbvfo 3883  mapprc 4324  map0b 4341  mapsn 4343  brdomg 4372  fodomr 4477  mapdom2lem 4487  fodomfi 4554  fodomfib 4555  inf3lem7 4607  fodom 4786  fodomb 4788  fseqsupcl 6485  fseqsupub 6486  infmap2 7538  iscnp2 7718  cnpco 7726  iscncl 7727  cnsscnp 7729  cncnplem4 7734  cnconst 7737  ismet 7755  dfms2 7756  metssba 7766  metne0 7778  metreslem 7779  metres 7780  metcnplem 7843  metcnp 7844  metcnp3 7853  metcnss 7855  metcnss2 7856  grprndm 8011  resgrprn 8052  subgres 8074  vcoprne 8155  nvdm 8246  imsdval 8274  imsba 8278  ipfval 8309  sspn 8352  dmadjrnb 9785  ghomfo 10346  mapdiscn 10453  dcsda 10578

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 3191  df-f 3192

Copyright terms: Public domain