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

Theorem fndm 5685
Description: The domain of a function. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fndm  |-  ( F  Fn  A  ->  dom  F  =  A )

Proof of Theorem fndm
StepHypRef Expression
1 df-fn 5592 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
21simprbi 471 1  |-  ( F  Fn  A  ->  dom  F  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1452   dom cdm 4839   Fun wfun 5583    Fn wfn 5584
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 378  df-fn 5592
This theorem is referenced by:  funfni  5686  fndmu  5687  fnbr  5688  fnco  5694  fnresdm  5695  fnresdisj  5696  fnssresb  5698  fn0  5705  fnimadisj  5706  fnimaeq0  5707  dmmpti  5717  fdm  5745  f1dm  5796  f1odm  5832  f1o00  5861  fvelimab  5936  fvun1  5951  eqfnfv2  5992  fndmdif  6001  fneqeql2  6006  elpreima  6017  fsn2  6078  fnprb  6139  fntpb  6140  fconst3  6144  fconst4  6145  fnfvima  6161  fnunirn  6176  dff13  6177  nvof1o  6197  f1eqcocnv  6217  oprssov  6457  offval  6557  ofrfval  6558  fnexALT  6778  dmmpt2  6882  dmmpt2ga  6884  curry1  6907  curry1val  6908  curry2  6910  curry2val  6912  fparlem3  6917  fparlem4  6918  fnwelem  6930  suppvalfn  6940  suppfnss  6959  fnsuppres  6961  tposfo2  7014  wfrlem3  7055  wfrlem4  7057  wfrdmcl  7062  wfrlem12  7065  wfrlem17  7070  smodm2  7092  smoel2  7100  tfrlem5  7116  tfrlem8  7120  tfrlem9  7121  tfrlem9a  7122  tfrlem13  7126  tfr2  7134  tz7.44-2  7143  tz7.44-3  7144  rdgsuc  7160  rdglim  7162  frsucmptn  7174  tz7.48-2  7177  tz7.48-1  7178  tz7.48-3  7179  tz7.49  7180  brwitnlem  7227  om0x  7239  oaabs2  7364  omabs  7366  elpmi  7508  elmapex  7510  pmresg  7517  pmsspw  7524  ixpprc  7561  undifixp  7576  bren  7596  fndmeng  7664  wemapso  8084  ixpiunwdom  8124  inf0  8144  r1suc  8259  r1lim  8261  r1ord  8269  r1ord3  8271  jech9.3  8303  onwf  8319  ssrankr1  8324  r1val3  8327  r1pw  8334  rankuni  8352  rankr1b  8353  alephcard  8519  alephnbtwn  8520  alephgeom  8531  dfac3  8570  dfac12lem1  8591  dfac12lem2  8592  cda1dif  8624  cdacomen  8629  cdadom1  8634  cdainf  8640  pwcdadom  8664  ackbij2lem3  8689  cfsmolem  8718  alephsing  8724  fin23lem31  8791  itunisuc  8867  itunitc1  8868  ituniiun  8870  hsmexlem6  8879  zorn2lem4  8947  ttukeylem3  8959  alephadd  9020  alephreg  9025  pwcfsdom  9026  cfpwsdom  9027  r1limwun  9179  r1wunlim  9180  rankcf  9220  inatsk  9221  r1tskina  9225  grur1  9263  dmaddpi  9333  dmmulpi  9334  genpdm  9445  fsuppmapnn0fiublem  12240  fsuppmapnn0fiub  12241  hashkf  12555  hashfn  12592  wrdlndm  12734  cshimadifsn  12985  cshimadifsn0  12986  shftfn  13213  rlimi2  13655  bpolylem  14178  phimullem  14806  0rest  15406  restsspw  15408  firest  15409  prdsbas2  15445  prdsplusgval  15449  prdsmulrval  15451  prdsleval  15453  prdsdsval  15454  prdsvscaval  15455  imasleval  15525  xpsfrnel2  15549  homfeqbas  15679  cidpropd  15693  2oppchomf  15707  sscpwex  15798  sscfn1  15800  sscfn2  15801  ssclem  15802  isssc  15803  rescval2  15811  issubc2  15819  cofuval  15865  resfval2  15876  resf1st  15877  resf2nd  15878  funcres  15879  fucbas  15943  fuchom  15944  xpcbas  16141  xpchomfval  16142  xpccofval  16145  oppchofcl  16223  oyoncl  16233  gsumpropd2lem  16594  frmdss2  16725  gicer  17018  psgndmsubg  17221  psgneldm  17222  psgneldm2  17223  psgnval  17226  prdsmgp  17916  lspextmo  18357  psgnghm  19225  psgnghm2  19226  dsmmbas2  19377  dsmmfi  19378  dsmmelbas  19379  frlmsslsp  19431  islindf4  19473  ofco2  19553  cldrcl  20118  iscldtop  20188  neiss2  20194  restrcl  20250  restbas  20251  ssrest  20269  resstopn  20279  ptval  20662  txdis1cn  20727  qtopcld  20805  qtoprest  20809  kqsat  20823  kqdisj  20824  kqcldsat  20825  isr0  20829  kqnrmlem1  20835  kqnrmlem2  20836  hmphtop  20870  hmpher  20876  elfm3  21043  ustn0  21313  nghmfval  21805  isnghm  21806  nghmfvalOLD  21823  isnghmOLD  21824  ovolunlem1  22528  uniiccdif  22614  cpncn  22969  cpnres  22970  ulmf2  23418  tglngne  24674  uhgraun  25117  umgraf  25124  vdgrfval  25702  eupai  25774  eupap1  25783  ghabloOLD  26178  fcoinver  28290  ofpreima  28343  ofpreima2  28344  fnct  28372  mdetpmtr1  28723  ofcfval  28993  probfinmeasb  29335  coinflipspace  29386  bnj564  29626  bnj945  29657  bnj545  29778  bnj548  29780  bnj570  29788  bnj900  29812  bnj929  29819  bnj983  29834  bnj1018  29845  bnj1110  29863  bnj1121  29866  bnj1145  29874  bnj1245  29895  bnj1253  29898  bnj1286  29900  bnj1280  29901  bnj1296  29902  bnj1311  29905  bnj1442  29930  bnj1450  29931  bnj1498  29942  bnj1514  29944  bnj1501  29948  cvmtop1  30055  cvmtop2  30056  dfrdg2  30513  frrlem3  30587  frrlem4  30588  frrlem5e  30593  frrlem11  30597  imageval  30768  filnetlem4  31108  sdclem2  32135  prdstotbnd  32190  heibor1lem  32205  diadm  34674  dibdiadm  34794  dibdmN  34796  dicdmN  34823  dihdm  34908  ismrc  35614  dnnumch3lem  35975  dnnumch3  35976  aomclem4  35986  aomclem6  35988  fnchoice  37413  fnresdmss  37504  wessf1ornlem  37530  icccncfext  37862  stoweidlem35  38008  stoweidlem59  38032  fnresfnco  38772  fdisjdmun  38775  fnbrafvb  38801  uhgrn0  39311  upgrfn  39333  upgrex  39338  umgrfn  39344  uhgun  40200  fnxpdmdm  40276  plusfreseq  40280
  Copyright terms: Public domain W3C validator