Theorem fdm 4567

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

Syntax hints:   -> wi 3   = wceq 1298  dom cdm 3986   Fn wfn 3993  -->wf 3994

This theorem is referenced by:  fdmi 4568  fcoOLD 4574  fssxp 4575  fssxpOLD 4576  ffdm 4578  dmfex 4598  dmfexOLD 4599  f00 4601  foima 4622  fornex 4625  foco 4628  f1ores 4654  f1imacnv 4656  resdif 4659  f1ococnv2 4662  fimacnv 4783  dff3 4790  fopab2 4796  cbvfo 4861  mapprc 5385  map0b 5402  mapsn 5404  brdomg 5435  ac6sfilem3 5508  fodomr 5547  mapdom2lem 5587  fodomfi 5656  fodomfib 5657  inf3lem7 5725  fodom 5960  fodomb 5962  fseqsupcl 7704  fseqsupubi 7705  infmap2 8850  iscnp2 9037  cnpnei 9043  cnpco 9046  iscncl 9047  cnsscnp 9049  cncnplem4 9054  cnconst 9057  ismet 9075  dfms2 9076  metssba 9086  metn0 9098  metreslem 9099  metres 9100  metcnplem 9164  metcnp 9165  metcnp3 9174  metcnss 9176  metcnss2 9177  grprndm 9334  resgrprn 9403  subgres 9426  isga 9450  isga2 9452  ssga 9455  gapmlem 9461  vcoprne 9530  nvdm 9621  imsdval 9649  imsba 9653  ipfval 9691  sspn 9734  basmetres 10185  tx1cn 10223  tx2cn 10224  upxp 10225  uptx 10226  txcnopab 10228  subtopmetlem 10255  ismgm 10367  ismnd2 10392  rnplrnml0 10402  dmadjrnb 11467  ghomfo 13634  soseq 13955  nodmon 13994  axbday 14012  bdaydm 14015  axdenselem2 14020  injrec 14461  surjsec 14462  surjsec2 14467  fopab2g 14485  islatalg 14531  dmrngrp 14699  mgmrddd 14727  symgfo 14730  curgrpact 14735  rngmgmbs3 14766  rnplrnml3 14768  zintdom 14787  svs3 14830  mapdiscnlem 14870  istopx 14918  bwt2 14960  topgrpbs 14974  lvsovso 15038  supnuf 15041  dcsda 15080  morcat 15127  cncls 15419  cnntr 15420  cnsubsp 15426  ivthALT 15454  cnpfillim 15589  rnelfmlem 15592  rnelfm 15593  fmfnfmlem2 15595  fmfnfmlem4 15597  fmfnfm 15598  cocanfo 15689  f1ocan1fv 15717  upixp 15729  indexdom 15754  cnss 15892  paste 15893  ismtyhmeolem 15950  ismtyres 15954  heiborlem33 15987  heiborlem34 15988  exidreslem 16030  isablda 16035  ghomco 16040  grpkerinj 16042  reparpht 16065  pi1set 16096  divrngcl 16110  isdivrng2 16111  keridl 16180  smoiso 16453  addcomgi 16455

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 164  df-an 242  df-fn 4009  df-f 4010

Copyright terms: Public domain