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

Theorem fndm 5359
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 5274 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
21simprbi 450 1  |-  ( F  Fn  A  ->  dom  F  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   dom cdm 4705   Fun wfun 5265    Fn wfn 5266
This theorem is referenced by:  funfni  5360  fndmu  5361  fnbr  5362  fnco  5368  fnresdm  5369  fnresdisj  5370  fnssresb  5372  fn0  5379  fnimadisj  5380  fnimaeq0  5381  dmmpti  5389  fdm  5409  f1dm  5457  f1odm  5492  f1o00  5524  fvelimab  5594  fvun1  5606  eqfnfv2  5639  fndmdif  5645  fneqeql2  5650  elpreima  5661  fsn2  5714  fconst3  5751  fconst4  5752  fnexALT  5758  fnfvima  5772  fnunirn  5794  dff13  5799  f1eqcocnv  5821  oprssov  6005  offval  6101  ofrfval  6102  dmmpt2  6210  curry1  6226  curry1val  6227  curry2  6229  curry2val  6231  fparlem3  6236  fparlem4  6237  fnwelem  6246  tposfo2  6273  smodm2  6388  smoel2  6396  tfrlem8  6416  tfrlem9  6417  tfrlem9a  6418  tfrlem13  6422  tfr2  6430  tz7.44-2  6436  tz7.44-3  6437  rdgsuc  6453  rdglim  6455  frsucmptn  6467  tz7.48-2  6470  tz7.48-1  6471  tz7.48-3  6472  tz7.49  6473  brwitnlem  6522  om0x  6534  oaabs2  6659  omabs  6661  elpmi  6805  elmapex  6807  pmresg  6811  pmsspw  6818  ixpprc  6853  undifixp  6868  bren  6887  fndmeng  6953  wemapso  7282  ixpiunwdom  7321  inf0  7338  noinfepOLD  7377  r1suc  7458  r1lim  7460  r1ord  7468  r1ord3  7470  jech9.3  7502  onwf  7518  ssrankr1  7523  r1val3  7526  r1pw  7533  rankuni  7551  rankr1b  7552  alephcard  7713  alephnbtwn  7714  alephgeom  7725  dfac3  7764  dfac12lem1  7785  dfac12lem2  7786  cda1dif  7818  cdacomen  7823  cdadom1  7828  cdainf  7834  pwcdadom  7858  ackbij2lem3  7883  cfsmolem  7912  alephsing  7918  fin23lem31  7985  itunisuc  8061  itunitc1  8062  ituniiun  8064  hsmexlem6  8073  zorn2lem4  8142  ttukeylem3  8154  alephadd  8215  alephreg  8220  pwcfsdom  8221  cfpwsdom  8222  r1limwun  8374  r1wunlim  8375  rankcf  8415  inatsk  8416  r1tskina  8420  grur1  8458  dmaddpi  8530  dmmulpi  8531  genpdm  8642  hashkf  11355  hashfn  11373  shftfn  11584  rlimi2  12004  rlimmptrcl  12097  phimullem  12863  0rest  13350  restsspw  13352  firest  13353  prdsbas2  13384  prdsplusgval  13388  prdsmulrval  13390  prdsleval  13392  prdsdsval  13393  prdsvscaval  13394  imasleval  13459  xpsfrnel2  13483  homfeqbas  13615  cidpropd  13629  2oppchomf  13643  sscpwex  13708  sscfn1  13710  sscfn2  13711  ssclem  13712  isssc  13713  rescval2  13721  issubc2  13729  cofuval  13772  resfval2  13783  resf1st  13784  resf2nd  13785  funcres  13786  fullfunc  13796  fthfunc  13797  natfval  13836  fucbas  13850  fuchom  13851  xpcbas  13968  xpchomfval  13969  xpccofval  13972  oppchofcl  14050  oyoncl  14060  frmdss2  14501  gicer  14756  prdsmgp  15409  lspextmo  15829  cldrcl  16779  iscldtop  16848  neiss2  16854  restrcl  16904  restbas  16905  ssrest  16923  resstopn  16932  ptval  17281  txdis1cn  17345  qtopcld  17420  qtoprest  17424  kqsat  17438  kqdisj  17439  kqcldsat  17440  isr0  17444  kqnrmlem1  17450  kqnrmlem2  17451  hmphtop  17485  hmpher  17491  elfm3  17661  nghmfval  18247  isnghm  18248  ovolunlem1  18872  uniiccdif  18949  iblcnlem  19159  cpncn  19301  cpnres  19302  dvmptres3  19321  ulmf2  19779  ghablo  21052  nvof1o  23052  fnct  23356  gsumpropd2lem  23394  ofcfval  23474  indf1ofs  23624  probfinmeasb  23647  coinflipspace  23696  cvmtop1  23806  cvmtop2  23807  umgraf  23885  eupai  23898  vdgrfval  23904  eupap1  23915  dfrdg2  24223  wfrlem3  24329  wfrlem4  24330  wfrlem9  24335  wfrlem12  24338  frrlem3  24354  frrlem4  24355  frrlem5e  24360  frrlem11  24364  imageval  24540  bpolylem  24855  imfstnrelc  25184  npincppr  25262  repfuntw  25263  prl2  25272  cur1vald  25302  domrancur1b  25303  domrancur1c  25305  valcurfn1  25307  nsn  25633  valdom  25987  fnctartar  26010  fnctartar2  26011  filnetlem4  26433  sdclem2  26555  prdstotbnd  26621  heibor1lem  26636  ismrc  26879  dnnumch3lem  27246  dnnumch3  27247  aomclem4  27257  aomclem6  27259  dsmmbas2  27306  dsmmfi  27307  dsmmelbas  27308  frlmsslsp  27351  frlmlbs  27352  islindf4  27411  psgndmsubg  27528  psgneldm  27529  psgneldm2  27530  psgnval  27533  psgnghm  27540  psgnghm2  27541  fnchoice  27803  stoweidlem35  27887  stoweidlem59  27911  dmmpt2g  28086  fnresfnco  28094  fnbrafvb  28122  bnj564  29089  bnj945  29121  bnj545  29243  bnj548  29245  bnj570  29253  bnj900  29277  bnj929  29284  bnj983  29299  bnj1018  29310  bnj1110  29328  bnj1121  29331  bnj1145  29339  bnj1245  29360  bnj1253  29363  bnj1286  29365  bnj1280  29366  bnj1296  29367  bnj1311  29370  bnj1442  29395  bnj1450  29396  bnj1498  29407  bnj1514  29409  bnj1501  29413  diadm  31847  dibdiadm  31967  dibdmN  31969  dicdmN  31996  dihdm  32081
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-fn 5274
  Copyright terms: Public domain W3C validator