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

Theorem fndm 5890
Description: The domain of a function. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fndm (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)

Proof of Theorem fndm
StepHypRef Expression
1 df-fn 5793 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simprbi 478 1 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  dom cdm 5028  Fun wfun 5784   Fn wfn 5785
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 195  df-an 384  df-fn 5793
This theorem is referenced by:  funfni  5891  fndmu  5892  fnbr  5893  fnco  5899  fnresdm  5900  fnresdisj  5901  fnssresb  5903  fn0  5910  fnimadisj  5911  fnimaeq0  5912  dmmpti  5922  fdm  5950  f1dm  6003  f1odm  6039  f1o00  6068  fvelimab  6148  fvun1  6164  eqfnfv2  6205  fndmdif  6214  fneqeql2  6219  elpreima  6230  fsn2  6294  fnprb  6355  fntpb  6356  fconst3  6360  fconst4  6361  fnfvima  6378  fnunirn  6393  dff13  6394  nvof1o  6414  f1eqcocnv  6434  oprssov  6678  offval  6779  ofrfval  6780  fnexALT  7002  dmmpt2  7106  dmmpt2ga  7108  curry1  7133  curry1val  7134  curry2  7136  curry2val  7138  fparlem3  7143  fparlem4  7144  fnwelem  7156  suppvalfn  7166  suppfnss  7184  fnsuppres  7186  tposfo2  7239  wfrlem3  7280  wfrlem4  7282  wfrdmcl  7287  wfrlem12  7290  wfrlem17  7295  smodm2  7316  smoel2  7324  tfrlem5  7340  tfrlem8  7344  tfrlem9  7345  tfrlem9a  7346  tfrlem13  7350  tfr2  7358  tz7.44-2  7367  tz7.44-3  7368  rdgsuc  7384  rdglim  7386  frsucmptn  7398  tz7.48-2  7401  tz7.48-1  7402  tz7.48-3  7403  tz7.49  7404  brwitnlem  7451  om0x  7463  oaabs2  7589  omabs  7591  elpmi  7739  elmapex  7741  pmresg  7748  pmsspw  7755  ixpprc  7792  undifixp  7807  bren  7827  fndmeng  7896  wemapso  8316  ixpiunwdom  8356  inf0  8378  r1suc  8493  r1lim  8495  r1ord  8503  r1ord3  8505  jech9.3  8537  onwf  8553  ssrankr1  8558  r1val3  8561  r1pw  8568  rankuni  8586  rankr1b  8587  alephcard  8753  alephnbtwn  8754  alephgeom  8765  dfac3  8804  dfac12lem1  8825  dfac12lem2  8826  cda1dif  8858  cdacomen  8863  cdadom1  8868  cdainf  8874  pwcdadom  8898  ackbij2lem3  8923  cfsmolem  8952  alephsing  8958  fin23lem31  9025  itunisuc  9101  itunitc1  9102  ituniiun  9104  hsmexlem6  9113  zorn2lem4  9181  ttukeylem3  9193  alephadd  9255  alephreg  9260  pwcfsdom  9261  cfpwsdom  9262  r1limwun  9414  r1wunlim  9415  rankcf  9455  inatsk  9456  r1tskina  9460  grur1  9498  dmaddpi  9568  dmmulpi  9569  genpdm  9680  fsuppmapnn0fiublem  12606  fsuppmapnn0fiub  12607  fsuppmapnn0fiubOLD  12608  hashkf  12936  hashfn  12977  wrdlndm  13122  cshimadifsn  13372  cshimadifsn0  13373  shftfn  13607  rlimi2  14039  bpolylem  14564  phimullem  15268  0rest  15859  restsspw  15861  firest  15862  prdsbas2  15898  prdsplusgval  15902  prdsmulrval  15904  prdsleval  15906  prdsdsval  15907  prdsvscaval  15908  imasleval  15970  xpsfrnel2  15994  homfeqbas  16125  cidpropd  16139  2oppchomf  16153  sscpwex  16244  sscfn1  16246  sscfn2  16247  ssclem  16248  isssc  16249  rescval2  16257  issubc2  16265  cofuval  16311  resfval2  16322  resf1st  16323  resf2nd  16324  funcres  16325  fucbas  16389  fuchom  16390  xpcbas  16587  xpchomfval  16588  xpccofval  16591  oppchofcl  16669  oyoncl  16679  gsumpropd2lem  17042  frmdss2  17169  gicer  17487  gicerOLD  17488  psgndmsubg  17691  psgneldm  17692  psgneldm2  17693  psgnval  17696  prdsmgp  18379  lspextmo  18823  psgnghm  19690  psgnghm2  19691  dsmmbas2  19842  dsmmfi  19843  dsmmelbas  19844  frlmsslsp  19896  islindf4  19938  ofco2  20018  cldrcl  20582  iscldtop  20651  neiss2  20657  restrcl  20713  restbas  20714  ssrest  20732  resstopn  20742  ptval  21125  txdis1cn  21190  qtopcld  21268  qtoprest  21272  kqsat  21286  kqdisj  21287  kqcldsat  21288  isr0  21292  kqnrmlem1  21298  kqnrmlem2  21299  hmphtop  21333  hmpher  21339  elfm3  21506  ustn0  21776  nghmfval  22268  isnghm  22269  ovolunlem1  22989  uniiccdif  23069  cpncn  23422  cpnres  23423  ulmf2  23859  tglngne  25163  uhgraun  25606  umgraf  25613  vdgrfval  26188  eupai  26260  eupap1  26269  fcoinver  28604  ofpreima  28654  ofpreima2  28655  fnct  28682  mdetpmtr1  29023  ofcfval  29293  probfinmeasb  29624  coinflipspace  29675  bnj564  29874  bnj945  29904  bnj545  30025  bnj548  30027  bnj570  30035  bnj900  30059  bnj929  30066  bnj983  30081  bnj1018  30092  bnj1110  30110  bnj1121  30113  bnj1145  30121  bnj1245  30142  bnj1253  30145  bnj1286  30147  bnj1280  30148  bnj1296  30149  bnj1311  30152  bnj1442  30177  bnj1450  30178  bnj1498  30189  bnj1514  30191  bnj1501  30195  cvmtop1  30302  cvmtop2  30303  dfrdg2  30751  frrlem3  30832  frrlem4  30833  frrlem5e  30838  frrlem11  30842  imageval  31013  filnetlem4  31352  sdclem2  32504  prdstotbnd  32559  heibor1lem  32574  diadm  35138  dibdiadm  35258  dibdmN  35260  dicdmN  35287  dihdm  35372  ismrc  36078  dnnumch3lem  36430  dnnumch3  36431  aomclem4  36441  aomclem6  36443  ntrclsfv1  37169  ntrneifv1  37193  fnchoice  38007  fnresdmss  38138  wessf1ornlem  38162  icccncfext  38570  stoweidlem35  38725  stoweidlem59  38749  fnresfnco  39652  fdisjdmun  39655  fnbrafvb  39681  uhgrn0  40284  upgrfn  40308  upgrex  40313  umgrfn  40319  fnxpdmdm  41553  plusfreseq  41557
  Copyright terms: Public domain W3C validator