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

Theorem fndm 5693
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 5604 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
21simprbi 465 1  |-  ( F  Fn  A  ->  dom  F  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   dom cdm 4854   Fun wfun 5595    Fn wfn 5596
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 188  df-an 372  df-fn 5604
This theorem is referenced by:  funfni  5694  fndmu  5695  fnbr  5696  fnco  5702  fnresdm  5703  fnresdisj  5704  fnssresb  5706  fn0  5713  fnimadisj  5714  fnimaeq0  5715  dmmpti  5725  fdm  5750  f1dm  5800  f1odm  5835  f1o00  5863  fvelimab  5937  fvun1  5952  eqfnfv2  5992  fndmdif  6001  fneqeql2  6006  elpreima  6017  fsn2  6077  fnprb  6138  fconst3  6143  fconst4  6144  fnfvima  6158  fnunirn  6173  dff13  6174  nvof1o  6194  f1eqcocnv  6214  oprssov  6452  offval  6552  ofrfval  6553  fnexALT  6773  dmmpt2  6877  dmmpt2ga  6879  curry1  6899  curry1val  6900  curry2  6902  curry2val  6904  fparlem3  6909  fparlem4  6910  fnwelem  6922  suppvalfn  6932  suppfnss  6951  fnsuppres  6953  tposfo2  7004  wfrlem3  7045  wfrlem4  7047  wfrdmcl  7052  wfrlem12  7055  wfrlem17  7060  smodm2  7082  smoel2  7090  tfrlem5  7106  tfrlem8  7110  tfrlem9  7111  tfrlem9a  7112  tfrlem13  7116  tfr2  7124  tz7.44-2  7133  tz7.44-3  7134  rdgsuc  7150  rdglim  7152  frsucmptn  7164  tz7.48-2  7167  tz7.48-1  7168  tz7.48-3  7169  tz7.49  7170  brwitnlem  7217  om0x  7229  oaabs2  7354  omabs  7356  elpmi  7498  elmapex  7500  pmresg  7507  pmsspw  7514  ixpprc  7551  undifixp  7566  bren  7586  fndmeng  7653  wemapso  8066  ixpiunwdom  8106  inf0  8126  r1suc  8240  r1lim  8242  r1ord  8250  r1ord3  8252  jech9.3  8284  onwf  8300  ssrankr1  8305  r1val3  8308  r1pw  8315  rankuni  8333  rankr1b  8334  alephcard  8499  alephnbtwn  8500  alephgeom  8511  dfac3  8550  dfac12lem1  8571  dfac12lem2  8572  cda1dif  8604  cdacomen  8609  cdadom1  8614  cdainf  8620  pwcdadom  8644  ackbij2lem3  8669  cfsmolem  8698  alephsing  8704  fin23lem31  8771  itunisuc  8847  itunitc1  8848  ituniiun  8850  hsmexlem6  8859  zorn2lem4  8927  ttukeylem3  8939  alephadd  9000  alephreg  9005  pwcfsdom  9006  cfpwsdom  9007  r1limwun  9160  r1wunlim  9161  rankcf  9201  inatsk  9202  r1tskina  9206  grur1  9244  dmaddpi  9314  dmmulpi  9315  genpdm  9426  fsuppmapnn0fiublem  12199  fsuppmapnn0fiub  12200  hashkf  12514  hashfn  12551  shftfn  13115  rlimi2  13556  bpolylem  14079  phimullem  14687  0rest  15278  restsspw  15280  firest  15281  prdsbas2  15317  prdsplusgval  15321  prdsmulrval  15323  prdsleval  15325  prdsdsval  15326  prdsvscaval  15327  imasleval  15389  xpsfrnel2  15413  homfeqbas  15543  cidpropd  15557  2oppchomf  15571  sscpwex  15662  sscfn1  15664  sscfn2  15665  ssclem  15666  isssc  15667  rescval2  15675  issubc2  15683  cofuval  15729  resfval2  15740  resf1st  15741  resf2nd  15742  funcres  15743  fucbas  15807  fuchom  15808  xpcbas  16005  xpchomfval  16006  xpccofval  16009  oppchofcl  16087  oyoncl  16097  gsumpropd2lem  16458  frmdss2  16589  gicer  16882  psgndmsubg  17085  psgneldm  17086  psgneldm2  17087  psgnval  17090  prdsmgp  17764  lspextmo  18205  psgnghm  19070  psgnghm2  19071  dsmmbas2  19222  dsmmfi  19223  dsmmelbas  19224  frlmsslsp  19276  islindf4  19318  ofco2  19398  cldrcl  19963  iscldtop  20033  neiss2  20039  restrcl  20095  restbas  20096  ssrest  20114  resstopn  20124  ptval  20507  txdis1cn  20572  qtopcld  20650  qtoprest  20654  kqsat  20668  kqdisj  20669  kqcldsat  20670  isr0  20674  kqnrmlem1  20680  kqnrmlem2  20681  hmphtop  20715  hmpher  20721  elfm3  20887  ustn0  21157  nghmfval  21645  isnghm  21646  ovolunlem1  22319  uniiccdif  22403  cpncn  22758  cpnres  22759  ulmf2  23195  tglngne  24446  uhgraun  24875  umgraf  24882  vdgrfval  25459  eupai  25531  eupap1  25540  ghabloOLD  25933  fcoinver  28044  ofpreima  28099  ofpreima2  28100  fnct  28131  mdetpmtr1  28479  ofcfval  28749  probfinmeasb  29079  coinflipspace  29130  bnj564  29333  bnj945  29364  bnj545  29485  bnj548  29487  bnj570  29495  bnj900  29519  bnj929  29526  bnj983  29541  bnj1018  29552  bnj1110  29570  bnj1121  29573  bnj1145  29581  bnj1245  29602  bnj1253  29605  bnj1286  29607  bnj1280  29608  bnj1296  29609  bnj1311  29612  bnj1442  29637  bnj1450  29638  bnj1498  29649  bnj1514  29651  bnj1501  29655  cvmtop1  29762  cvmtop2  29763  dfrdg2  30220  frrlem3  30294  frrlem4  30295  frrlem5e  30300  frrlem11  30304  imageval  30473  filnetlem4  30813  sdclem2  31765  prdstotbnd  31820  heibor1lem  31835  diadm  34302  dibdiadm  34422  dibdmN  34424  dicdmN  34451  dihdm  34536  ismrc  35242  dnnumch3lem  35600  dnnumch3  35601  aomclem4  35611  aomclem6  35613  fnchoice  36980  fnresdmss  37043  wessf1ornlem  37072  icccncfext  37327  stoweidlem35  37455  stoweidlem59  37479  fnresfnco  38008  fnbrafvb  38036  uhgun  38440  fnxpdmdm  38516  plusfreseq  38520
  Copyright terms: Public domain W3C validator