MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fdm Structured version   Visualization version   GIF version

Theorem fdm 6038
Description: The domain of a mapping. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fdm (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)

Proof of Theorem fdm
StepHypRef Expression
1 ffn 6032 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fndm 5978 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2syl 17 1 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  dom cdm 5104   Fn wfn 5871  wf 5872
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 197  df-an 386  df-fn 5879  df-f 5880
This theorem is referenced by:  fdmi  6039  fssxp  6047  ffdm  6049  f00  6074  f0dom0  6076  f0rn0  6077  foima  6107  foco  6112  resdif  6144  fimacnv  6333  dff3  6358  ffvresb  6380  fmptco  6382  dmfex  7109  fornex  7120  frnsuppeq  7292  suppss  7310  onnseq  7426  issmo2  7431  smoiso  7444  mapprc  7846  elpm2r  7860  map0b  7881  mapsn  7884  brdomg  7950  pw2f1olem  8049  fopwdom  8053  fodomfib  8225  fisuppfi  8268  intrnfi  8307  ordtypelem5  8412  ordtypelem6  8413  ordtypelem7  8414  ordtypelem8  8415  wemapso2lem  8442  brwdomn0  8459  wdomtr  8465  cantnfcl  8549  cantnfle  8553  cantnflt  8554  cantnff  8556  cantnfp1lem3  8562  cantnflem1b  8568  cantnflem1d  8570  cantnflem1  8571  cantnflem3  8573  cnfcomlem  8581  cnfcom  8582  cnfcom2lem  8583  cnfcom3lem  8585  cnfcom3  8586  iunmapdisj  8831  fseqenlem2  8833  fodomfi2  8868  infmap2  9025  coftr  9080  fin23lem30  9149  fin23lem40  9158  isf34lem5  9185  isf34lem7  9186  isf34lem6  9187  fin1a2lem7  9213  axdc3lem2  9258  axdc3lem4  9260  ttukeylem6  9321  fodomb  9333  pwxpndom2  9472  rpnnen1lem4  11802  rpnnen1lem5  11803  rpnnen1lem4OLD  11808  rpnnen1lem5OLD  11809  fseqsupcl  12759  fseqsupubi  12760  hashf1lem1  13222  wrddm  13295  swrdcl  13401  swrdnd2  13415  cats1un  13457  repswswrd  13512  limsupgle  14189  limsupgre  14193  rlim  14207  rlimi  14225  ello12  14228  lo1bdd  14232  elo12  14239  o1bdd  14243  lo1o1  14244  rlimclim  14258  rlimuni  14262  o1co  14298  rlimcn1  14300  isercolllem2  14377  isercolllem3  14378  fsumss  14437  fprodss  14659  ruclem11  14950  1arith  15612  vdwlem1  15666  vdwlem5  15670  vdwlem6  15671  vdwlem11  15676  ramval  15693  0ram  15705  0ram2  15706  0ramcl  15708  mrcuni  16262  homarcl2  16666  prfval  16820  intopsn  17234  gsumval  17252  gsumval2  17261  ghmrn  17654  ghmpreima  17663  cntzmhm2  17753  symgfixf1  17838  f1omvdconj  17847  pmtrfconj  17867  pmtrdifellem1  17877  pmtrdifellem2  17878  gsumval3lem1  18287  gsumval3lem2  18288  gsumval3  18289  gsumzres  18291  gsumzcl2  18292  gsumzf1o  18294  gsumzaddlem  18302  gsumzmhm  18318  gsumzoppg  18325  gsum2d  18352  dmdprdd  18379  dprdres  18408  dprdss  18409  dprdf1  18413  dmdprdsplitlem  18417  dprd2da  18422  dmdprdsplit2lem  18425  dmdprdsplit2  18426  dmdprdsplit  18427  dprdsplit  18428  dpjidcl  18438  ablfac1eulem  18452  ablfac1eu  18453  ablfaclem2  18466  ablfaclem3  18467  ablfac2  18469  lmhmpreima  19029  lmhmlsp  19030  mplcoe1  19446  mplcoe5  19449  psr1baslem  19536  gsumfsum  19794  evpmss  19913  regsumsupp  19949  pjdm2  20036  frlmlbs  20117  islindf2  20134  f1lindf  20142  islindf4  20158  mattpostpos  20241  mdetdiaglem  20385  decpmatval  20551  pmatcollpw3lem  20569  iinopn  20688  iscnp3  21029  lmbrf  21045  cnpnei  21049  cnclima  21053  iscncl  21054  cnntri  21056  cnclsi  21057  cncls2  21058  cncls  21059  cnntr  21060  cncnp  21065  cndis  21076  paste  21079  lmcnp  21089  cnt0  21131  cnt1  21135  cnhaus  21139  cncmp  21176  imacmp  21181  hauscmplem  21190  cnconn  21206  connima  21209  1stcfb  21229  1stccnp  21246  1stckgenlem  21337  kgencn  21340  kgencn3  21342  txcnpi  21392  txcnp  21404  txcnmpt  21408  prdstps  21413  xkohaus  21437  xkopt  21439  xkoco2cn  21442  xkococnlem  21443  qtopval2  21480  qtopcn  21498  qtopeu  21500  hmeores  21555  fbasrn  21669  fmval  21728  fmf  21730  rnelfmlem  21737  rnelfm  21738  fmfnfmlem2  21740  fmfnfmlem4  21742  fmfnfm  21743  cnflf2  21788  lmflf  21790  txflf  21791  cnextfval  21847  cnextcn  21852  clssubg  21893  ghmcnp  21899  tgphaus  21901  qustgplem  21905  tsmsval  21915  tsmsgsum  21923  ucncn  22070  psmetdmdm  22091  xmetdmdm  22121  metn0  22146  xmetres  22150  metres  22151  xmeter  22219  tmsval  22267  metcnp  22327  metustss  22337  metustid  22340  metustsym  22341  metustexhalf  22342  metustfbas  22343  cfilucfil  22345  metuel2  22351  restmetu  22356  isngp2  22382  evth  22739  lmmbrf  23041  iscfil2  23045  caufval  23054  iscau2  23056  iscauf  23059  caucfil  23062  equivcau  23079  lmclimf  23083  rrxcph  23161  rrxsuppss  23167  ovollb2  23238  ovolunlem1a  23245  ovoliunlem1  23251  ovoliun2  23255  ioombl1lem4  23310  uniioombllem1  23330  uniioombllem2  23332  uniioombllem6  23337  mbfconstlem  23377  ismbf  23378  ismbfcn  23379  mbfimaicc  23381  mbfmulc2lem  23395  mbfmulc2re  23396  mbfimaopn2  23405  cncombf  23406  mbfaddlem  23408  mbflimsup  23414  i1f0rn  23430  itg1addlem5  23448  itg1climres  23462  mbfmullem2  23472  ibl0  23534  cniccibl  23588  limcfval  23617  limcdif  23621  ellimc2  23622  ellimc3  23624  limccnp  23636  dvfval  23642  cpnord  23679  cpnres  23681  dvcmul  23688  dvcmulf  23689  dvnfre  23696  dvexp  23697  c1liplem1  23740  c1lip2  23742  dvgt0lem1  23746  dvcnvrelem1  23761  dvcnvrelem2  23762  mdegfval  23803  mdegleb  23805  mdegldg  23807  deg1mul3le  23857  plyco0  23929  plyeq0lem  23947  plyeq0  23948  plyaddlem1  23950  plymullem1  23951  dgrcl  23970  dgrub  23971  dgrlb  23973  plycpn  24025  vieta1lem1  24046  vieta1lem2  24047  aalioulem3  24070  taylfvallem1  24092  tayl0  24097  taylply2  24103  taylply  24104  dvtaylp  24105  dvntaylp  24106  dvntaylp0  24107  taylthlem1  24108  taylthlem2  24109  ulm2  24120  ulmss  24132  ulmdvlem1  24135  ulmdvlem2  24136  ulmdvlem3  24137  itgulm  24143  xrlimcnp  24676  basellem5  24792  dchrelbas2  24943  dchrghm  24962  dchrptlem1  24970  dchrptlem2  24971  iscgrgd  25389  iscgrglt  25390  trgcgrg  25391  tgcgr4  25407  motcgrg  25420  eedimeq  25759  axcontlem10  25834  wrdupgr  25961  wrdumgr  25973  upgr1e  25989  wlkn0  26497  wlkres  26548  wlkp1lem1  26551  pthdivtx  26606  grporndm  27334  sspn  27561  dmadjrnb  28735  elnlfn  28757  xppreima  29422  fmptcof2  29430  curry2ima  29460  fpwrelmap  29482  smatrcl  29836  mdetpmtr1  29863  locfinreflem  29881  hauseqcn  29915  rge0scvg  29969  indpreima  30061  indf1ofs  30062  esumpcvgval  30114  ofcfval4  30141  isrnmeas  30237  measdivcst  30262  omsfval  30330  omscl  30331  omsf  30332  oms0  30333  omsmon  30334  omssubaddlem  30335  omssubadd  30336  carsgval  30339  carsggect  30354  omsmeas  30359  sibfof  30376  sitgclg  30378  eulerpartlemsv2  30394  eulerpartlemsf  30395  eulerpartlemv  30400  eulerpartlemd  30402  eulerpartlemb  30404  eulerpartlemt  30407  eulerpartlemr  30410  eulerpartlemgvv  30412  eulerpartlemgu  30413  eulerpartlemgs2  30416  eulerpartlemn  30417  sseqfv2  30430  rrvdm  30482  rpsqrtcn  30645  ftc2re  30650  cvmliftmolem1  31237  cvmliftlem3  31243  cvmliftlem10  31250  cvmliftlem13  31252  cvmlift2lem9  31267  cvmlift3lem6  31280  cvmlift3lem7  31281  mrsubfval  31379  mclsax  31440  mclsppslem  31454  mclspps  31455  soseq  31725  nodmon  31777  fwddifval  32244  fwddifnval  32245  ivthALT  32305  bj-finsumval0  33118  curf  33358  uncf  33359  curunc  33362  unccur  33363  matunitlindflem2  33377  ptrecube  33380  heicant  33415  mbfresfi  33427  itg2addnclem  33432  itg2addnclem2  33433  cnicciblnc  33452  ftc1anclem1  33456  ftc1anclem5  33460  ftc1anclem6  33461  ftc1anclem8  33463  indexdom  33500  sdclem2  33509  cnres2  33533  sstotbnd2  33544  isbnd3  33554  ssbnd  33558  bnd2lem  33561  ismtyval  33570  ismgmOLD  33620  ismndo2  33644  exidreslem  33647  grpokerinj  33663  rngosn3  33694  rngodm1dm2  33702  divrngcl  33727  isdrngo2  33728  keridl  33802  ismrcd1  37080  istopclsd  37082  mapfzcons2  37101  coeq0i  37135  pw2f1ocnv  37423  fnwe2lem2  37440  lmhmfgima  37473  pwfi2f1o  37485  cnioobibld  37618  itgpowd  37619  wnefimgd  38280  funfvima2d  38289  binomcxplemnotnn0  38375  cncmpmax  39011  fresin2  39168  mapsnd  39204  fdmd  39236  evthiccabs  39521  mullimcf  39655  cncfuni  39862  cncficcgt0  39864  cncfioobd  39873  dvsinax  39890  dvsubcncf  39902  dvmulcncf  39903  dvdivcncf  39905  cnbdibl  39941  itgperiod  39960  fvvolioof  39969  fvvolicof  39971  stoweidlem29  40009  fourierdlem20  40107  fourierdlem48  40134  fourierdlem49  40135  fourierdlem53  40139  fourierdlem58  40144  fourierdlem59  40145  fourierdlem63  40149  fourierdlem68  40154  fourierdlem71  40157  fourierdlem73  40159  fourierdlem74  40160  fourierdlem75  40161  fourierdlem76  40162  fourierdlem80  40166  fourierdlem81  40167  fourierdlem82  40168  fourierdlem89  40175  fourierdlem91  40177  fourierdlem92  40178  fourierdlem93  40179  fourierdlem94  40180  fourierdlem111  40197  fourierdlem112  40198  fourierdlem113  40199  fouriercn  40212  sge0val  40346  fge0iccico  40350  sge0sn  40359  sge0tsms  40360  sge0cl  40361  sge0f1o  40362  sge0isum  40407  ismeannd  40447  isomennd  40508  hoicvr  40525  dmovn  40581  hspmbl  40606  ovolval4lem1  40626  ovnovollem1  40633  ovnovollem2  40634  fmtnoinf  41213  nnsum4primeseven  41453  nnsum4primesevenALTV  41454  domnmsuppn0  41915  rmsuppss  41916  mndpsuppss  41917  scmsuppss  41918  fdivmpt  42099  fdivmptf  42100  refdivmptf  42101  fdivpm  42102  refdivpm  42103  elbigo2  42111  elbigolo1  42116
  Copyright terms: Public domain W3C validator