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

Theorem fndm 5503
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 5416 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
21simprbi 451 1  |-  ( F  Fn  A  ->  dom  F  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   dom cdm 4837   Fun wfun 5407    Fn wfn 5408
This theorem is referenced by:  funfni  5504  fndmu  5505  fnbr  5506  fnco  5512  fnresdm  5513  fnresdisj  5514  fnssresb  5516  fn0  5523  fnimadisj  5524  fnimaeq0  5525  dmmpti  5533  fdm  5554  f1dm  5602  f1odm  5637  f1o00  5669  fvelimab  5741  fvun1  5753  eqfnfv2  5787  fndmdif  5793  fneqeql2  5798  elpreima  5809  fsn2  5867  fnpr  5909  fnprOLD  5910  fconst3  5914  fconst4  5915  fnexALT  5921  fnfvima  5935  fnunirn  5958  dff13  5963  f1eqcocnv  5987  oprssov  6174  offval  6271  ofrfval  6272  dmmpt2  6380  curry1  6397  curry1val  6398  curry2  6400  curry2val  6402  fparlem3  6407  fparlem4  6408  fnwelem  6420  tposfo2  6461  smodm2  6576  smoel2  6584  tfrlem8  6604  tfrlem9  6605  tfrlem9a  6606  tfrlem13  6610  tfr2  6618  tz7.44-2  6624  tz7.44-3  6625  rdgsuc  6641  rdglim  6643  frsucmptn  6655  tz7.48-2  6658  tz7.48-1  6659  tz7.48-3  6660  tz7.49  6661  brwitnlem  6710  om0x  6722  oaabs2  6847  omabs  6849  elpmi  6994  elmapex  6996  pmresg  7000  pmsspw  7007  ixpprc  7042  undifixp  7057  bren  7076  fndmeng  7142  wemapso  7476  ixpiunwdom  7515  inf0  7532  noinfepOLD  7571  r1suc  7652  r1lim  7654  r1ord  7662  r1ord3  7664  jech9.3  7696  onwf  7712  ssrankr1  7717  r1val3  7720  r1pw  7727  rankuni  7745  rankr1b  7746  alephcard  7907  alephnbtwn  7908  alephgeom  7919  dfac3  7958  dfac12lem1  7979  dfac12lem2  7980  cda1dif  8012  cdacomen  8017  cdadom1  8022  cdainf  8028  pwcdadom  8052  ackbij2lem3  8077  cfsmolem  8106  alephsing  8112  fin23lem31  8179  itunisuc  8255  itunitc1  8256  ituniiun  8258  hsmexlem6  8267  zorn2lem4  8335  ttukeylem3  8347  alephadd  8408  alephreg  8413  pwcfsdom  8414  cfpwsdom  8415  r1limwun  8567  r1wunlim  8568  rankcf  8608  inatsk  8609  r1tskina  8613  grur1  8651  dmaddpi  8723  dmmulpi  8724  genpdm  8835  hashkf  11575  hashfn  11604  shftfn  11843  rlimi2  12263  rlimmptrcl  12356  phimullem  13123  0rest  13612  restsspw  13614  firest  13615  prdsbas2  13646  prdsplusgval  13650  prdsmulrval  13652  prdsleval  13654  prdsdsval  13655  prdsvscaval  13656  imasleval  13721  xpsfrnel2  13745  homfeqbas  13877  cidpropd  13891  2oppchomf  13905  sscpwex  13970  sscfn1  13972  sscfn2  13973  ssclem  13974  isssc  13975  rescval2  13983  issubc2  13991  cofuval  14034  resfval2  14045  resf1st  14046  resf2nd  14047  funcres  14048  fucbas  14112  fuchom  14113  xpcbas  14230  xpchomfval  14231  xpccofval  14234  oppchofcl  14312  oyoncl  14322  frmdss2  14763  gicer  15018  prdsmgp  15671  lspextmo  16087  cldrcl  17045  iscldtop  17114  neiss2  17120  restrcl  17175  restbas  17176  ssrest  17194  resstopn  17204  ptval  17555  txdis1cn  17620  qtopcld  17698  qtoprest  17702  kqsat  17716  kqdisj  17717  kqcldsat  17718  isr0  17722  kqnrmlem1  17728  kqnrmlem2  17729  hmphtop  17763  hmpher  17769  elfm3  17935  ustn0  18203  nghmfval  18709  isnghm  18710  ovolunlem1  19346  uniiccdif  19423  iblcnlem  19633  cpncn  19775  cpnres  19776  dvmptres3  19795  ulmf2  20253  uhgraun  21299  umgraf  21306  vdgrfval  21619  eupai  21642  eupap1  21651  ghablo  21910  nvof1o  23993  ofpreima  24034  fnct  24058  gsumpropd2lem  24173  ofcfval  24434  probfinmeasb  24640  coinflipspace  24691  cvmtop1  24900  cvmtop2  24901  dfrdg2  25366  wfrlem3  25472  wfrlem4  25473  wfrlem9  25478  wfrlem12  25481  frrlem3  25497  frrlem4  25498  frrlem5e  25503  frrlem11  25507  imageval  25683  bpolylem  25998  filnetlem4  26300  sdclem2  26336  prdstotbnd  26393  heibor1lem  26408  ismrc  26645  dnnumch3lem  27011  dnnumch3  27012  aomclem4  27022  aomclem6  27024  dsmmbas2  27071  dsmmfi  27072  dsmmelbas  27073  frlmsslsp  27116  frlmlbs  27117  islindf4  27176  psgndmsubg  27293  psgneldm  27294  psgneldm2  27295  psgnval  27298  psgnghm  27305  psgnghm2  27306  fnchoice  27567  stoweidlem35  27651  stoweidlem59  27675  dmmpt2g  27850  fnresfnco  27857  fnbrafvb  27885  bnj564  28818  bnj945  28850  bnj545  28972  bnj548  28974  bnj570  28982  bnj900  29006  bnj929  29013  bnj983  29028  bnj1018  29039  bnj1110  29057  bnj1121  29060  bnj1145  29068  bnj1245  29089  bnj1253  29092  bnj1286  29094  bnj1280  29095  bnj1296  29096  bnj1311  29099  bnj1442  29124  bnj1450  29125  bnj1498  29136  bnj1514  29138  bnj1501  29142  diadm  31518  dibdiadm  31638  dibdmN  31640  dicdmN  31667  dihdm  31752
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 178  df-an 361  df-fn 5416
  Copyright terms: Public domain W3C validator