Theorem fdm 5756

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

Syntax hints:   -> wi 4   = wceq 1455   dom cdm 4853   Fn wfn 5596   -->wf 5597

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

This theorem depends on definitions:  df-bi 190  df-an 377  df-fn 5604  df-f 5605

This theorem is referenced by:  fdmi  5757  fssxp  5764  ffdm  5766  f00  5788  f0dom0  5790  f0rn0  5791  foima  5821  foco  5826  resdif  5857  fimacnv  6035  dff3  6058  ffvresb  6078  fmptco  6080  dmfex  6778  fornex  6789  frnsuppeq  6953  suppss  6972  onnseq  7089  issmo2  7094  smoiso  7107  mapprc  7502  elpm2r  7515  map0b  7536  mapsn  7539  brdomg  7605  pw2f1olem  7702  fopwdom  7706  fodomfib  7877  fisuppfi  7917  intrnfi  7956  ordtypelem5  8063  ordtypelem6  8064  ordtypelem7  8065  ordtypelem8  8066  wemapso2lem  8093  brwdomn0  8110  wdomtr  8116  cantnfcl  8198  cantnfle  8202  cantnflt  8203  cantnff  8205  cantnfp1lem3  8211  cantnflem1b  8217  cantnflem1d  8219  cantnflem1  8220  cantnflem3  8222  cnfcomlem  8230  cnfcom  8231  cnfcom2lem  8232  cnfcom3lem  8234  cnfcom3  8235  iunmapdisj  8480  fseqenlem2  8482  fodomfi2  8517  infmap2  8674  coftr  8729  fin23lem30  8798  fin23lem40  8807  isf34lem5  8834  isf34lem7  8835  isf34lem6  8836  fin1a2lem7  8862  axdc3lem2  8907  axdc3lem4  8909  ttukeylem6  8970  fodomb  8980  pwxpndom2  9116  rpnnen1lem4  11322  rpnnen1lem5  11323  fseqsupcl  12222  fseqsupubi  12223  hashimarn  12643  hashfzdm  12645  hashfirdm  12647  hashf1lem1  12651  wrddm  12711  swrdcl  12812  swrdnd2  12826  cats1un  12869  repswswrd  12924  limsupgle  13584  limsupgre  13591  limsupgreOLD  13592  rlim  13608  rlimi  13626  ello12  13629  lo1bdd  13633  elo12  13640  o1bdd  13644  lo1o1  13645  rlimclim  13659  rlimuni  13663  o1co  13699  rlimcn1  13701  isercolllem2  13778  isercolllem3  13779  fsumss  13840  fprodss  14051  ruclem11  14341  1arith  14920  vdwlem1  14980  vdwlem5  14984  vdwlem6  14985  vdwlem11  14990  ramval  15009  ramvalOLD  15010  0ram  15027  0ram2  15028  0ramcl  15030  mrcuni  15576  homarcl2  15979  prfval  16133  intopsn  16547  gsumval  16563  gsumval2  16572  ghmrn  16945  ghmpreima  16953  cntzmhm2  17042  symgfixf1  17127  f1omvdconj  17136  pmtrfconj  17156  pmtrdifellem1  17166  pmtrdifellem2  17167  gsumval3lem1  17588  gsumval3lem2  17589  gsumval3  17590  gsumzres  17592  gsumzcl2  17593  gsumzf1o  17595  gsumzaddlem  17603  gsumzmhm  17619  gsumzoppg  17626  gsum2d  17653  dmdprdd  17680  dprdres  17710  dprdss  17711  dprdf1  17715  dmdprdsplitlem  17719  dprd2da  17724  dmdprdsplit2lem  17727  dmdprdsplit2  17728  dmdprdsplit  17729  dprdsplit  17730  dpjidcl  17740  ablfac1eulem  17754  ablfac1eu  17755  ablfaclem2  17768  ablfaclem3  17769  ablfac2  17771  lmhmpreima  18320  lmhmlsp  18321  mplcoe1  18738  mplcoe5  18741  psr1baslem  18827  gsumfsum  19083  evpmss  19203  regsumsupp  19239  pjdm2  19323  frlmlbs  19404  islindf2  19421  f1lindf  19429  islindf4  19445  mattpostpos  19528  mdetdiaglem  19672  decpmatval  19838  pmatcollpw3lem  19856  iinopn  19981  iscnp3  20309  lmbrf  20325  cnpnei  20329  cnclima  20333  iscncl  20334  cnntri  20336  cnclsi  20337  cncls2  20338  cncls  20339  cnntr  20340  cncnp  20345  cndis  20356  paste  20359  lmcnp  20369  cnt0  20411  cnt1  20415  cnhaus  20419  cncmp  20456  imacmp  20461  hauscmplem  20470  cnconn  20486  conima  20489  1stcfb  20509  1stccnp  20526  1stckgenlem  20617  kgencn  20620  kgencn3  20622  txcnpi  20672  txcnp  20684  txcnmpt  20688  prdstps  20693  xkohaus  20717  xkopt  20719  xkoco2cn  20722  xkococnlem  20723  qtopval2  20760  qtopcn  20778  qtopeu  20780  hmeores  20835  fbasrn  20948  fmval  21007  fmf  21009  rnelfmlem  21016  rnelfm  21017  fmfnfmlem2  21019  fmfnfmlem4  21021  fmfnfm  21022  cnflf2  21067  lmflf  21069  txflf  21070  cnextfval  21126  cnextcn  21131  clssubg  21172  ghmcnp  21178  tgphaus  21180  qustgplem  21184  tsmsval  21194  tsmsgsum  21202  ucncn  21349  psmetdmdm  21370  xmetdmdm  21399  metn0  21424  xmetres  21428  metres  21429  xmeter  21497  tmsval  21545  metcnp  21605  metustss  21615  metustid  21618  metustsym  21619  metustexhalf  21620  metustfbas  21621  cfilucfil  21623  metuel2  21629  restmetu  21634  isngp2  21660  evth  22036  lmmbrf  22281  iscfil2  22285  caufval  22294  iscau2  22296  iscauf  22299  caucfil  22302  equivcau  22319  lmclimf  22322  rrxcph  22400  rrxsuppss  22406  ovollb2  22491  ovolunlem1a  22498  ovoliunlem1  22504  ovoliun2  22508  ioombl1lem4  22563  uniioombllem1  22587  uniioombllem2  22589  uniioombllem2OLD  22590  uniioombllem6  22595  mbfconstlem  22634  ismbf  22635  ismbfcn  22636  mbfimaicc  22638  mbfmulc2lem  22652  mbfmulc2re  22653  mbfimaopn2  22662  cncombf  22663  mbfaddlem  22665  mbflimsup  22672  mbflimsupOLD  22673  i1f0rn  22689  itg1addlem5  22707  itg1climres  22721  mbfmullem2  22731  ibl0  22793  cniccibl  22847  limcfval  22876  limcdif  22880  ellimc2  22881  ellimc3  22883  limccnp  22895  dvfval  22901  cpnord  22938  cpnres  22940  dvcmul  22947  dvcmulf  22948  dvnfre  22955  dvexp  22956  c1liplem1  22997  c1lip2  22999  dvgt0lem1  23003  dvcnvrelem1  23018  dvcnvrelem2  23019  mdegfval  23060  mdegleb  23062  mdegldg  23064  deg1mul3le  23114  plyco0  23195  plyeq0lem  23213  plyeq0  23214  plyaddlem1  23216  plymullem1  23217  dgrcl  23236  dgrub  23237  dgrlb  23239  plycpn  23291  vieta1lem1  23312  vieta1lem2  23313  aalioulem3  23339  taylfvallem1  23361  tayl0  23366  taylply2  23372  taylply  23373  dvtaylp  23374  dvntaylp  23375  dvntaylp0  23376  taylthlem1  23377  taylthlem2  23378  ulm2  23389  ulmss  23401  ulmdvlem1  23404  ulmdvlem2  23405  ulmdvlem3  23406  itgulm  23412  xrlimcnp  23943  basellem5  24060  dchrelbas2  24214  dchrghm  24233  dchrptlem1  24241  dchrptlem2  24242  iscgrgd  24607  iscgrglt  24608  trgcgrg  24609  tgcgr4  24625  motcgrg  24638  eedimeq  24977  axcontlem10  25052  uhgraun  25087  wrdumgra  25092  umgra1  25102  umgraun  25104  wlkn0  25304  eupares  25752  grporndm  25987  resgrprn  26057  isabloda  26076  subgores  26081  ismgmOLD  26097  ismndo2  26122  ghsubgolemOLD  26147  rngodm1dm2  26195  rngosn3  26203  vcoprne  26247  nvdm  26339  sspn  26424  dmadjrnb  27608  elnlfn  27630  xppreima  28297  fmptcof2  28308  curry2ima  28338  fpwrelmap  28367  smatrcl  28671  mdetpmtr1  28698  locfinreflem  28716  hauseqcn  28750  rge0scvg  28804  indpreima  28895  indf1ofs  28896  esumpcvgval  28948  ofcfval4  28975  isrnmeas  29071  measdivcst  29096  omsfval  29167  omscl  29168  omsf  29169  omsfvalOLD  29171  omsclOLD  29172  omsfOLD  29173  oms0  29174  omsmon  29175  omssubaddlem  29176  omssubadd  29177  oms0OLD  29178  omsmonOLD  29179  omssubaddlemOLD  29180  omssubaddOLD  29181  carsgval  29184  carsggect  29199  omsmeas  29204  omsmeasOLD  29205  sibfof  29222  sitgclg  29224  eulerpartlemsv2  29240  eulerpartlemsf  29241  eulerpartlemv  29246  eulerpartlemd  29248  eulerpartlemb  29250  eulerpartlemt  29253  eulerpartlemr  29256  eulerpartlemgvv  29258  eulerpartlemgu  29259  eulerpartlemgs2  29262  eulerpartlemn  29263  sseqfv2  29276  rrvdm  29328  cvmliftmolem1  30053  cvmliftlem3  30059  cvmliftlem10  30066  cvmliftlem13  30068  cvmlift2lem9  30083  cvmlift3lem6  30096  cvmlift3lem7  30097  mrsubfval  30195  mclsax  30256  mclsppslem  30270  mclspps  30271  ghomfo  30358  soseq  30541  nodmon  30586  fwddifval  30978  fwddifnval  30979  ivthALT  31040  bj-finsumval0  31747  ptrecube  31985  heicant  32020  mbfresfi  32032  itg2addnclem  32038  itg2addnclem2  32039  cnicciblnc  32058  ftc1anclem1  32062  ftc1anclem5  32066  ftc1anclem6  32067  ftc1anclem8  32069  indexdom  32106  sdclem2  32116  cnres2  32140  sstotbnd2  32151  isbnd3  32161  ssbnd  32165  bnd2lem  32168  ismtyval  32177  exidreslem  32220  grpokerinj  32228  divrngcl  32241  isdrngo2  32242  keridl  32310  ismrcd1  35585  istopclsd  35587  mapfzcons2  35606  coeq0i  35640  pw2f1ocnv  35937  fnwe2lem2  35954  lmhmfgima  35987  pwfi2f1o  35999  cnioobibld  36143  itgpowd  36144  wnefimgd  36645  funfvima2d  36657  binomcxplemnotnn0  36749  cncmpmax  37393  fresin2  37474  mapsnd  37514  evthiccabs  37631  mullimcf  37741  cncfuni  37802  cncficcgt0  37804  cncfioobd  37813  dvsinax  37821  dvsubcncf  37834  dvmulcncf  37835  dvdivcncf  37837  cnbdibl  37877  itgperiod  37896  stoweidlem29  37927  stoweidlem29OLD  37928  fourierdlem20  38027  fourierdlem48  38056  fourierdlem49  38057  fourierdlem53  38061  fourierdlem58  38066  fourierdlem59  38067  fourierdlem63  38071  fourierdlem68  38076  fourierdlem71  38079  fourierdlem73  38081  fourierdlem74  38082  fourierdlem75  38083  fourierdlem76  38084  fourierdlem80  38088  fourierdlem81  38089  fourierdlem82  38090  fourierdlem89  38097  fourierdlem91  38099  fourierdlem92  38100  fourierdlem93  38101  fourierdlem94  38102  fourierdlem111  38119  fourierdlem112  38120  fourierdlem113  38121  fouriercn  38134  sge0val  38246  fge0iccico  38250  sge0sn  38259  sge0tsms  38260  sge0cl  38261  sge0f1o  38262  sge0isum  38307  ismeannd  38343  isomennd  38390  hoicvr  38408  dmovn  38464  hspmbl  38489  nnsum4primeseven  38933  nnsum4primesevenALTV  38934  uhgrun  39214  wrdupgr  39224  wrdumgr  39234  upgr1e  39249  upgrun  39254  umgrun  39256  1wlkn0  39685  pthdivtx  39762  uhgun  39965  domnmsuppn0  40427  rmsuppss  40428  mndpsuppss  40429  scmsuppss  40430  fdivmpt  40624  fdivmptf  40625  refdivmptf  40626  fdivpm  40627  refdivpm  40628  elbigo2  40636  elbigolo1  40641