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 4853   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  7007  wfrlem3  7048  wfrlem4  7050  wfrdmcl  7055  wfrlem12  7058  wfrlem17  7063  smodm2  7085  smoel2  7093  tfrlem5  7109  tfrlem8  7113  tfrlem9  7114  tfrlem9a  7115  tfrlem13  7119  tfr2  7127  tz7.44-2  7136  tz7.44-3  7137  rdgsuc  7153  rdglim  7155  frsucmptn  7167  tz7.48-2  7170  tz7.48-1  7171  tz7.48-3  7172  tz7.49  7173  brwitnlem  7220  om0x  7232  oaabs2  7357  omabs  7359  elpmi  7501  elmapex  7503  pmresg  7510  pmsspw  7517  ixpprc  7554  undifixp  7569  bren  7589  fndmeng  7656  wemapso  8075  ixpiunwdom  8115  inf0  8135  r1suc  8249  r1lim  8251  r1ord  8259  r1ord3  8261  jech9.3  8293  onwf  8309  ssrankr1  8314  r1val3  8317  r1pw  8324  rankuni  8342  rankr1b  8343  alephcard  8508  alephnbtwn  8509  alephgeom  8520  dfac3  8559  dfac12lem1  8580  dfac12lem2  8581  cda1dif  8613  cdacomen  8618  cdadom1  8623  cdainf  8629  pwcdadom  8653  ackbij2lem3  8678  cfsmolem  8707  alephsing  8713  fin23lem31  8780  itunisuc  8856  itunitc1  8857  ituniiun  8859  hsmexlem6  8868  zorn2lem4  8936  ttukeylem3  8948  alephadd  9009  alephreg  9014  pwcfsdom  9015  cfpwsdom  9016  r1limwun  9168  r1wunlim  9169  rankcf  9209  inatsk  9210  r1tskina  9214  grur1  9252  dmaddpi  9322  dmmulpi  9323  genpdm  9434  fsuppmapnn0fiublem  12208  fsuppmapnn0fiub  12209  hashkf  12523  hashfn  12560  shftfn  13136  rlimi2  13577  bpolylem  14100  phimullem  14726  0rest  15327  restsspw  15329  firest  15330  prdsbas2  15366  prdsplusgval  15370  prdsmulrval  15372  prdsleval  15374  prdsdsval  15375  prdsvscaval  15376  imasleval  15446  xpsfrnel2  15470  homfeqbas  15600  cidpropd  15614  2oppchomf  15628  sscpwex  15719  sscfn1  15721  sscfn2  15722  ssclem  15723  isssc  15724  rescval2  15732  issubc2  15740  cofuval  15786  resfval2  15797  resf1st  15798  resf2nd  15799  funcres  15800  fucbas  15864  fuchom  15865  xpcbas  16062  xpchomfval  16063  xpccofval  16066  oppchofcl  16144  oyoncl  16154  gsumpropd2lem  16515  frmdss2  16646  gicer  16939  psgndmsubg  17142  psgneldm  17143  psgneldm2  17144  psgnval  17147  prdsmgp  17837  lspextmo  18278  psgnghm  19146  psgnghm2  19147  dsmmbas2  19298  dsmmfi  19299  dsmmelbas  19300  frlmsslsp  19352  islindf4  19394  ofco2  19474  cldrcl  20039  iscldtop  20109  neiss2  20115  restrcl  20171  restbas  20172  ssrest  20190  resstopn  20200  ptval  20583  txdis1cn  20648  qtopcld  20726  qtoprest  20730  kqsat  20744  kqdisj  20745  kqcldsat  20746  isr0  20750  kqnrmlem1  20756  kqnrmlem2  20757  hmphtop  20791  hmpher  20797  elfm3  20963  ustn0  21233  nghmfval  21725  isnghm  21726  nghmfvalOLD  21743  isnghmOLD  21744  ovolunlem1  22448  uniiccdif  22533  cpncn  22888  cpnres  22889  ulmf2  23337  tglngne  24593  uhgraun  25036  umgraf  25043  vdgrfval  25621  eupai  25693  eupap1  25702  ghabloOLD  26095  fcoinver  28216  ofpreima  28270  ofpreima2  28271  fnct  28303  mdetpmtr1  28657  ofcfval  28927  probfinmeasb  29270  coinflipspace  29321  bnj564  29562  bnj945  29593  bnj545  29714  bnj548  29716  bnj570  29724  bnj900  29748  bnj929  29755  bnj983  29770  bnj1018  29781  bnj1110  29799  bnj1121  29802  bnj1145  29810  bnj1245  29831  bnj1253  29834  bnj1286  29836  bnj1280  29837  bnj1296  29838  bnj1311  29841  bnj1442  29866  bnj1450  29867  bnj1498  29878  bnj1514  29880  bnj1501  29884  cvmtop1  29991  cvmtop2  29992  dfrdg2  30449  frrlem3  30523  frrlem4  30524  frrlem5e  30529  frrlem11  30533  imageval  30702  filnetlem4  31042  sdclem2  32035  prdstotbnd  32090  heibor1lem  32105  diadm  34572  dibdiadm  34692  dibdmN  34694  dicdmN  34721  dihdm  34806  ismrc  35512  dnnumch3lem  35874  dnnumch3  35875  aomclem4  35885  aomclem6  35887  fnchoice  37323  fnresdmss  37391  wessf1ornlem  37420  icccncfext  37705  stoweidlem35  37836  stoweidlem59  37860  fnresfnco  38498  fnbrafvb  38526  uhgrn0  38985  uhgrunlem  38996  umgrf  39006  uhgun  39311  fnxpdmdm  39387  plusfreseq  39391
  Copyright terms: Public domain W3C validator