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

Theorem fdm 6089
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 6083 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fndm 6028 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2syl 17 1 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  dom cdm 5143   Fn wfn 5921  wf 5922
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 385  df-fn 5929  df-f 5930
This theorem is referenced by:  fdmi  6090  fssxp  6098  ffdm  6100  f00  6125  f0dom0  6127  f0rn0  6128  foima  6158  foco  6163  resdif  6195  fimacnv  6387  dff3  6412  ffvresb  6434  fmptco  6436  dmfex  7166  fornex  7177  frnsuppeq  7352  suppss  7370  onnseq  7486  issmo2  7491  smoiso  7504  mapprc  7903  elpm2r  7917  map0b  7938  mapsn  7941  brdomg  8007  pw2f1olem  8105  fopwdom  8109  fodomfib  8281  fisuppfi  8324  intrnfi  8363  ordtypelem5  8468  ordtypelem6  8469  ordtypelem7  8470  ordtypelem8  8471  wemapso2lem  8498  brwdomn0  8515  wdomtr  8521  cantnfcl  8602  cantnfle  8606  cantnflt  8607  cantnff  8609  cantnfp1lem3  8615  cantnflem1b  8621  cantnflem1d  8623  cantnflem1  8624  cantnflem3  8626  cnfcomlem  8634  cnfcom  8635  cnfcom2lem  8636  cnfcom3lem  8638  cnfcom3  8639  iunmapdisj  8884  fseqenlem2  8886  fodomfi2  8921  infmap2  9078  coftr  9133  fin23lem30  9202  fin23lem40  9211  isf34lem5  9238  isf34lem7  9239  isf34lem6  9240  fin1a2lem7  9266  axdc3lem2  9311  axdc3lem4  9313  ttukeylem6  9374  fodomb  9386  pwxpndom2  9525  rpnnen1lem4  11855  rpnnen1lem5  11856  rpnnen1lem4OLD  11861  rpnnen1lem5OLD  11862  fseqsupcl  12816  fseqsupubi  12817  hashf1lem1  13277  wrddm  13344  swrdcl  13464  swrdnd2  13479  cats1un  13521  repswswrd  13577  limsupgle  14252  limsupgre  14256  rlim  14270  rlimi  14288  ello12  14291  lo1bdd  14295  elo12  14302  o1bdd  14306  lo1o1  14307  rlimclim  14321  rlimuni  14325  o1co  14361  rlimcn1  14363  isercolllem2  14440  isercolllem3  14441  fsumss  14500  fprodss  14722  ruclem11  15013  1arith  15678  vdwlem1  15732  vdwlem5  15736  vdwlem6  15737  vdwlem11  15742  ramval  15759  0ram  15771  0ram2  15772  0ramcl  15774  mrcuni  16328  homarcl2  16732  prfval  16886  intopsn  17300  gsumval  17318  gsumval2  17327  ghmrn  17720  ghmpreima  17729  cntzmhm2  17818  symgfixf1  17903  f1omvdconj  17912  pmtrfconj  17932  pmtrdifellem1  17942  pmtrdifellem2  17943  gsumval3lem1  18352  gsumval3lem2  18353  gsumval3  18354  gsumzres  18356  gsumzcl2  18357  gsumzf1o  18359  gsumzaddlem  18367  gsumzmhm  18383  gsumzoppg  18390  gsum2d  18417  dmdprdd  18444  dprdres  18473  dprdss  18474  dprdf1  18478  dmdprdsplitlem  18482  dprd2da  18487  dmdprdsplit2lem  18490  dmdprdsplit2  18491  dmdprdsplit  18492  dprdsplit  18493  dpjidcl  18503  ablfac1eulem  18517  ablfac1eu  18518  ablfaclem2  18531  ablfaclem3  18532  ablfac2  18534  lmhmpreima  19096  lmhmlsp  19097  mplcoe1  19513  mplcoe5  19516  psr1baslem  19603  gsumfsum  19861  evpmss  19980  regsumsupp  20016  pjdm2  20103  frlmlbs  20184  islindf2  20201  f1lindf  20209  islindf4  20225  mattpostpos  20308  mdetdiaglem  20452  decpmatval  20618  pmatcollpw3lem  20636  iinopn  20755  iscnp3  21096  lmbrf  21112  cnpnei  21116  cnclima  21120  iscncl  21121  cnntri  21123  cnclsi  21124  cncls2  21125  cncls  21126  cnntr  21127  cncnp  21132  cndis  21143  paste  21146  lmcnp  21156  cnt0  21198  cnt1  21202  cnhaus  21206  cncmp  21243  imacmp  21248  hauscmplem  21257  cnconn  21273  connima  21276  1stcfb  21296  1stccnp  21313  1stckgenlem  21404  kgencn  21407  kgencn3  21409  txcnpi  21459  txcnp  21471  txcnmpt  21475  prdstps  21480  xkohaus  21504  xkopt  21506  xkoco2cn  21509  xkococnlem  21510  qtopval2  21547  qtopcn  21565  qtopeu  21567  hmeores  21622  fbasrn  21735  fmval  21794  fmf  21796  rnelfmlem  21803  rnelfm  21804  fmfnfmlem2  21806  fmfnfmlem4  21808  fmfnfm  21809  cnflf2  21854  lmflf  21856  txflf  21857  cnextfval  21913  cnextcn  21918  clssubg  21959  ghmcnp  21965  tgphaus  21967  qustgplem  21971  tsmsval  21981  tsmsgsum  21989  ucncn  22136  psmetdmdm  22157  xmetdmdm  22187  metn0  22212  xmetres  22216  metres  22217  xmeter  22285  tmsval  22333  metcnp  22393  metustss  22403  metustid  22406  metustsym  22407  metustexhalf  22408  metustfbas  22409  cfilucfil  22411  metuel2  22417  restmetu  22422  isngp2  22448  evth  22805  lmmbrf  23106  iscfil2  23110  caufval  23119  iscau2  23121  iscauf  23124  caucfil  23127  equivcau  23144  lmclimf  23148  rrxcph  23226  rrxsuppss  23232  ovollb2  23303  ovolunlem1a  23310  ovoliunlem1  23316  ovoliun2  23320  ioombl1lem4  23375  uniioombllem1  23395  uniioombllem2  23397  uniioombllem6  23402  mbfconstlem  23441  ismbf  23442  ismbfcn  23443  mbfimaicc  23445  mbfmulc2lem  23459  mbfmulc2re  23460  mbfimaopn2  23469  cncombf  23470  mbfaddlem  23472  mbflimsup  23478  i1f0rn  23494  itg1addlem5  23512  itg1climres  23526  mbfmullem2  23536  ibl0  23598  cniccibl  23652  limcfval  23681  limcdif  23685  ellimc2  23686  ellimc3  23688  limccnp  23700  dvfval  23706  cpnord  23743  cpnres  23745  dvcmul  23752  dvcmulf  23753  dvnfre  23760  dvexp  23761  c1liplem1  23804  c1lip2  23806  dvgt0lem1  23810  dvcnvrelem1  23825  dvcnvrelem2  23826  mdegfval  23867  mdegleb  23869  mdegldg  23871  deg1mul3le  23921  plyco0  23993  plyeq0lem  24011  plyeq0  24012  plyaddlem1  24014  plymullem1  24015  dgrcl  24034  dgrub  24035  dgrlb  24037  plycpn  24089  vieta1lem1  24110  vieta1lem2  24111  aalioulem3  24134  taylfvallem1  24156  tayl0  24161  taylply2  24167  taylply  24168  dvtaylp  24169  dvntaylp  24170  dvntaylp0  24171  taylthlem1  24172  taylthlem2  24173  ulm2  24184  ulmss  24196  ulmdvlem1  24199  ulmdvlem2  24200  ulmdvlem3  24201  itgulm  24207  xrlimcnp  24740  basellem5  24856  dchrelbas2  25007  dchrghm  25026  dchrptlem1  25034  dchrptlem2  25035  iscgrgd  25453  iscgrglt  25454  trgcgrg  25455  tgcgr4  25471  motcgrg  25484  eedimeq  25823  axcontlem10  25898  wrdupgr  26025  wrdumgr  26037  upgr1e  26053  wlkn0  26572  wlkres  26623  wlkp1lem1  26626  pthdivtx  26681  grporndm  27492  sspn  27719  dmadjrnb  28893  elnlfn  28915  xppreima  29577  fmptcof2  29585  curry2ima  29614  fpwrelmap  29636  smatrcl  29990  mdetpmtr1  30017  locfinreflem  30035  hauseqcn  30069  rge0scvg  30123  indpreima  30215  indf1ofs  30216  esumpcvgval  30268  ofcfval4  30295  isrnmeas  30391  measdivcst  30416  omsfval  30484  omscl  30485  omsf  30486  oms0  30487  omsmon  30488  omssubaddlem  30489  omssubadd  30490  carsgval  30493  carsggect  30508  omsmeas  30513  sibfof  30530  sitgclg  30532  eulerpartlemsv2  30548  eulerpartlemsf  30549  eulerpartlemv  30554  eulerpartlemd  30556  eulerpartlemb  30558  eulerpartlemt  30561  eulerpartlemr  30564  eulerpartlemgvv  30566  eulerpartlemgu  30567  eulerpartlemgs2  30570  eulerpartlemn  30571  sseqfv2  30584  rrvdm  30636  rpsqrtcn  30799  ftc2re  30804  cvmliftmolem1  31389  cvmliftlem3  31395  cvmliftlem10  31402  cvmliftlem13  31404  cvmlift2lem9  31419  cvmlift3lem6  31432  cvmlift3lem7  31433  mrsubfval  31531  mclsax  31592  mclsppslem  31606  mclspps  31607  soseq  31879  nodmon  31928  fwddifval  32394  fwddifnval  32395  ivthALT  32455  bj-finsumval0  33277  curf  33517  uncf  33518  curunc  33521  unccur  33522  matunitlindflem2  33536  ptrecube  33539  heicant  33574  mbfresfi  33586  itg2addnclem  33591  itg2addnclem2  33592  cnicciblnc  33611  ftc1anclem1  33615  ftc1anclem5  33619  ftc1anclem6  33620  ftc1anclem8  33622  indexdom  33659  sdclem2  33668  cnres2  33692  sstotbnd2  33703  isbnd3  33713  ssbnd  33717  bnd2lem  33720  ismtyval  33729  ismgmOLD  33779  ismndo2  33803  exidreslem  33806  grpokerinj  33822  rngosn3  33853  rngodm1dm2  33861  divrngcl  33886  isdrngo2  33887  keridl  33961  ismrcd1  37578  istopclsd  37580  mapfzcons2  37599  coeq0i  37633  pw2f1ocnv  37921  fnwe2lem2  37938  lmhmfgima  37971  pwfi2f1o  37983  cnioobibld  38116  itgpowd  38117  wnefimgd  38777  funfvima2d  38786  binomcxplemnotnn0  38872  cncmpmax  39505  fresin2  39666  mapsnd  39702  fdmd  39734  evthiccabs  40036  mullimcf  40173  cncfuni  40417  cncficcgt0  40419  cncfioobd  40428  dvsinax  40445  dvsubcncf  40457  dvmulcncf  40458  dvdivcncf  40460  cnbdibl  40496  itgperiod  40515  fvvolioof  40524  fvvolicof  40526  stoweidlem29  40564  fourierdlem20  40662  fourierdlem48  40689  fourierdlem49  40690  fourierdlem53  40694  fourierdlem58  40699  fourierdlem59  40700  fourierdlem63  40704  fourierdlem68  40709  fourierdlem71  40712  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem80  40721  fourierdlem81  40722  fourierdlem82  40723  fourierdlem89  40730  fourierdlem91  40732  fourierdlem92  40733  fourierdlem93  40734  fourierdlem94  40735  fourierdlem111  40752  fourierdlem112  40753  fourierdlem113  40754  fouriercn  40767  sge0val  40901  fge0iccico  40905  sge0sn  40914  sge0tsms  40915  sge0cl  40916  sge0f1o  40917  sge0isum  40962  ismeannd  41002  isomennd  41066  hoicvr  41083  dmovn  41139  hspmbl  41164  ovolval4lem1  41184  ovnovollem1  41191  ovnovollem2  41192  fmtnoinf  41773  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  domnmsuppn0  42475  rmsuppss  42476  mndpsuppss  42477  scmsuppss  42478  fdivmpt  42659  fdivmptf  42660  refdivmptf  42661  fdivpm  42662  refdivpm  42663  elbigo2  42671  elbigolo1  42676
  Copyright terms: Public domain W3C validator