Theorem fdm 3617

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

Syntax hints:   -> wi 3   = wceq 953  dom cdm 3160   Fn wfn 3167  -->wf 3168

This theorem is referenced by:  fco 3621  fssxp 3622  ffdm 3624  dmfex 3640  f00 3642  foima 3661  fornex 3664  foco 3667  f1ores 3688  f1imacnv 3690  f1ococnv2 3693  fimacnv 3795  dff2 3802  fopab2 3808  cbvfo 3870  mapprc 4310  map0b 4327  mapsn 4329  brdomg 4358  fodomr 4463  mapdom2lem 4473  fodomfi 4540  fodomfib 4541  inf3lem7 4591  fodom 4770  fodomb 4772  fseqsupcl 6457  fseqsupub 6458  climsup 7091  cvgcmpub 7121  unbenlem 7447  infmap2 7523  cnpco 7708  iscncl 7709  cnsscnp 7711  cncnplem4 7716  cnconst 7719  ismet 7737  dfms2 7738  ismeti 7741  metssba 7748  metreslem 7762  metres 7763  metcnplem 7825  metcnp 7826  metcnp3 7835  metcnss 7837  metcnss2 7838  cnmetdval 7841  cnmetba 7842  cncfmet 7844  cncfmet1 7845  remetba 7848  bcthlem29 7961  grprndm 7988  grprnOLD 7991  resgrprn 8030  subgres 8054  readdsubg 8066  zaddsubg 8067  ghsubgi 8075  vcoprne 8136  cnvc 8140  vsfval 8194  cnnv 8245  imsdval 8255  imsba 8259  abscncfALT 8278  ipfval 8286  sspn 8329  efghgrpilem 8634  shftefif1olem 8661  dfhnorm2 8909  hilvc 8950  hhssabl 9053  hhssnv 9054  hhshsslem1 9057  hoco 9607  dmadjrnb 9747  ghomfo 10296  clsrebb 10380  mapdiscn 10398  dcsda 10510

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 3183  df-f 3184

Copyright terms: Public domain