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

Theorem fndm 6028
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 5929 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simprbi 479 1 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  dom cdm 5143  Fun wfun 5920   Fn wfn 5921
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
This theorem is referenced by:  funfni  6029  fndmu  6030  fnbr  6031  fnco  6037  fnresdm  6038  fnresdisj  6039  fnssresb  6041  fn0  6049  fnimadisj  6050  fnimaeq0  6051  dmmpti  6061  fdm  6089  f1dm  6143  f1odm  6179  f1o00  6209  fvelimab  6292  fvun1  6308  eqfnfv2  6352  fndmdif  6361  fneqeql2  6366  elpreima  6377  fsn2  6443  fnprb  6513  fntpb  6514  fconst3  6518  fconst4  6519  fnfvima  6536  fnunirn  6551  dff13  6552  nvof1o  6576  f1eqcocnv  6596  oprssov  6845  offval  6946  ofrfval  6947  fnexALT  7174  dmmpt2  7285  dmmpt2ga  7287  curry1  7314  curry1val  7315  curry2  7317  curry2val  7319  fparlem3  7324  fparlem4  7325  fnwelem  7337  suppvalfn  7347  suppfnss  7365  fnsuppres  7367  tposfo2  7420  wfrlem3  7461  wfrlem4  7463  wfrdmcl  7468  wfrlem12  7471  wfrlem17  7476  smodm2  7497  smoel2  7505  tfrlem5  7521  tfrlem8  7525  tfrlem9  7526  tfrlem9a  7527  tfrlem13  7531  tfr2  7539  tz7.44-2  7548  tz7.44-3  7549  rdgsuc  7565  rdglim  7567  frsucmptn  7579  tz7.48-2  7582  tz7.48-1  7583  tz7.48-3  7584  tz7.49  7585  brwitnlem  7632  om0x  7644  oaabs2  7770  omabs  7772  elpmi  7918  elmapex  7920  pmresg  7927  pmsspw  7934  ixpprc  7971  undifixp  7986  bren  8006  fndmeng  8075  wemapso  8497  ixpiunwdom  8537  inf0  8556  r1suc  8671  r1lim  8673  r1ord  8681  r1ord3  8683  jech9.3  8715  onwf  8731  ssrankr1  8736  r1val3  8739  r1pw  8746  rankuni  8764  rankr1b  8765  alephcard  8931  alephnbtwn  8932  alephgeom  8943  dfac3  8982  dfac12lem1  9003  dfac12lem2  9004  cda1dif  9036  cdacomen  9041  cdadom1  9046  cdainf  9052  pwcdadom  9076  ackbij2lem3  9101  cfsmolem  9130  alephsing  9136  fin23lem31  9203  itunisuc  9279  itunitc1  9280  ituniiun  9282  hsmexlem6  9291  zorn2lem4  9359  ttukeylem3  9371  fnct  9397  alephadd  9437  alephreg  9442  pwcfsdom  9443  cfpwsdom  9444  r1limwun  9596  r1wunlim  9597  rankcf  9637  inatsk  9638  r1tskina  9642  grur1  9680  dmaddpi  9750  dmmulpi  9751  genpdm  9862  fsuppmapnn0fiublem  12829  fsuppmapnn0fiub  12830  fsuppmapnn0fiubOLD  12831  hashkf  13159  hashfn  13202  wrdlndm  13353  cshimadifsn  13621  cshimadifsn0  13622  shftfn  13857  rlimi2  14289  bpolylem  14823  phimullem  15531  0rest  16137  restsspw  16139  firest  16140  prdsbas2  16176  prdsplusgval  16180  prdsmulrval  16182  prdsleval  16184  prdsdsval  16185  prdsvscaval  16186  imasleval  16248  xpsfrnel2  16272  homfeqbas  16403  cidpropd  16417  2oppchomf  16431  sscpwex  16522  sscfn1  16524  sscfn2  16525  ssclem  16526  isssc  16527  rescval2  16535  issubc2  16543  cofuval  16589  resfval2  16600  resf1st  16601  resf2nd  16602  funcres  16603  fucbas  16667  fuchom  16668  xpcbas  16865  xpchomfval  16866  xpccofval  16869  oppchofcl  16947  oyoncl  16957  gsumpropd2lem  17320  frmdss2  17447  gicer  17765  psgndmsubg  17968  psgneldm  17969  psgneldm2  17970  psgnval  17973  prdsmgp  18656  lspextmo  19104  psgnghm  19974  psgnghm2  19975  dsmmbas2  20129  dsmmfi  20130  dsmmelbas  20131  frlmsslsp  20183  islindf4  20225  ofco2  20305  cldrcl  20878  iscldtop  20947  neiss2  20953  restrcl  21009  restbas  21010  ssrest  21028  resstopn  21038  ptval  21421  txdis1cn  21486  qtopcld  21564  qtoprest  21568  kqsat  21582  kqdisj  21583  kqcldsat  21584  isr0  21588  kqnrmlem1  21594  kqnrmlem2  21595  hmphtop  21629  hmpher  21635  elfm3  21801  ustn0  22071  nghmfval  22573  isnghm  22574  ovolunlem1  23311  uniiccdif  23392  cpncn  23744  cpnres  23745  ulmf2  24183  tglngne  25490  uhgrn0  26007  upgrfn  26027  upgrex  26032  umgrfn  26039  fnunres1  29543  fcoinver  29544  ofpreima  29593  ofpreima2  29594  mdetpmtr1  30017  ofcfval  30288  probfinmeasb  30619  coinflipspace  30670  bnj564  30940  bnj945  30970  bnj545  31091  bnj548  31093  bnj570  31101  bnj900  31125  bnj929  31132  bnj983  31147  bnj1018  31158  bnj1110  31176  bnj1121  31179  bnj1145  31187  bnj1245  31208  bnj1253  31211  bnj1286  31213  bnj1280  31214  bnj1296  31215  bnj1311  31218  bnj1442  31243  bnj1450  31244  bnj1498  31255  bnj1514  31257  bnj1501  31261  cvmtop1  31368  cvmtop2  31369  dfrdg2  31825  frrlem3  31907  frrlem4  31908  frrlem5e  31913  frrlem11  31917  imageval  32162  filnetlem4  32501  sdclem2  33668  prdstotbnd  33723  heibor1lem  33738  diadm  36641  dibdiadm  36761  dibdmN  36763  dicdmN  36790  dihdm  36875  ismrc  37581  dnnumch3lem  37933  dnnumch3  37934  aomclem4  37944  aomclem6  37946  ntrclsfv1  38670  ntrneifv1  38694  fnchoice  39502  fnresdmss  39662  wessf1ornlem  39685  fndmd  39755  icccncfext  40418  stoweidlem35  40570  stoweidlem59  40594  fnresfnco  41527  fnbrafvb  41555  fnxpdmdm  42093  plusfreseq  42097
  Copyright terms: Public domain W3C validator