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

Theorem fndm 5670
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 5581 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
21simprbi 464 1  |-  ( F  Fn  A  ->  dom  F  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383   dom cdm 4989   Fun wfun 5572    Fn wfn 5573
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 185  df-an 371  df-fn 5581
This theorem is referenced by:  funfni  5671  fndmu  5672  fnbr  5673  fnco  5679  fnresdm  5680  fnresdisj  5681  fnssresb  5683  fn0  5690  fnimadisj  5691  fnimaeq0  5692  dmmpti  5700  fdm  5725  f1dm  5775  f1odm  5810  f1o00  5838  fvelimab  5914  fvun1  5929  eqfnfv2  5967  fndmdif  5976  fneqeql2  5981  elpreima  5992  fsn2  6056  fnprb  6114  fnprOLD  6115  fconst3  6120  fconst4  6121  fnfvima  6135  fnunirn  6150  dff13  6151  nvof1o  6171  f1eqcocnv  6189  oprssov  6429  offval  6532  ofrfval  6533  fnexALT  6751  dmmpt2  6855  dmmpt2ga  6857  curry1  6877  curry1val  6878  curry2  6880  curry2val  6882  fparlem3  6887  fparlem4  6888  fnwelem  6900  suppvalfn  6910  suppfnss  6927  fnsuppres  6929  tposfo2  6980  smodm2  7028  smoel2  7036  tfrlem5  7051  tfrlem8  7055  tfrlem9  7056  tfrlem9a  7057  tfrlem13  7061  tfr2  7069  tz7.44-2  7075  tz7.44-3  7076  rdgsuc  7092  rdglim  7094  frsucmptn  7106  tz7.48-2  7109  tz7.48-1  7110  tz7.48-3  7111  tz7.49  7112  brwitnlem  7159  om0x  7171  oaabs2  7296  omabs  7298  elpmi  7439  elmapex  7441  pmresg  7448  pmsspw  7455  ixpprc  7492  undifixp  7507  bren  7527  fndmeng  7594  wemapso  7979  ixpiunwdom  8020  inf0  8041  noinfepOLD  8080  r1suc  8191  r1lim  8193  r1ord  8201  r1ord3  8203  jech9.3  8235  onwf  8251  ssrankr1  8256  r1val3  8259  r1pw  8266  rankuni  8284  rankr1b  8285  alephcard  8454  alephnbtwn  8455  alephgeom  8466  dfac3  8505  dfac12lem1  8526  dfac12lem2  8527  cda1dif  8559  cdacomen  8564  cdadom1  8569  cdainf  8575  pwcdadom  8599  ackbij2lem3  8624  cfsmolem  8653  alephsing  8659  fin23lem31  8726  itunisuc  8802  itunitc1  8803  ituniiun  8805  hsmexlem6  8814  zorn2lem4  8882  ttukeylem3  8894  alephadd  8955  alephreg  8960  pwcfsdom  8961  cfpwsdom  8962  r1limwun  9117  r1wunlim  9118  rankcf  9158  inatsk  9159  r1tskina  9163  grur1  9201  dmaddpi  9271  dmmulpi  9272  genpdm  9383  fsuppmapnn0fiublem  12078  fsuppmapnn0fiub  12079  hashkf  12389  hashfn  12425  shftfn  12888  rlimi2  13319  phimullem  14291  0rest  14809  restsspw  14811  firest  14812  prdsbas2  14848  prdsplusgval  14852  prdsmulrval  14854  prdsleval  14856  prdsdsval  14857  prdsvscaval  14858  imasleval  14920  xpsfrnel2  14944  homfeqbas  15073  cidpropd  15087  2oppchomf  15101  sscpwex  15166  sscfn1  15168  sscfn2  15169  ssclem  15170  isssc  15171  rescval2  15179  issubc2  15187  cofuval  15230  resfval2  15241  resf1st  15242  resf2nd  15243  funcres  15244  fucbas  15308  fuchom  15309  xpcbas  15426  xpchomfval  15427  xpccofval  15430  oppchofcl  15508  oyoncl  15518  gsumpropd2lem  15879  frmdss2  16010  gicer  16303  psgndmsubg  16506  psgneldm  16507  psgneldm2  16508  psgnval  16511  prdsmgp  17238  lspextmo  17681  psgnghm  18594  psgnghm2  18595  dsmmbas2  18746  dsmmfi  18747  dsmmelbas  18748  frlmsslsp  18807  frlmsslspOLD  18808  islindf4  18851  ofco2  18931  cldrcl  19505  iscldtop  19574  neiss2  19580  restrcl  19636  restbas  19637  ssrest  19655  resstopn  19665  ptval  20049  txdis1cn  20114  qtopcld  20192  qtoprest  20196  kqsat  20210  kqdisj  20211  kqcldsat  20212  isr0  20216  kqnrmlem1  20222  kqnrmlem2  20223  hmphtop  20257  hmpher  20263  elfm3  20429  ustn0  20701  nghmfval  21207  isnghm  21208  ovolunlem1  21886  uniiccdif  21965  cpncn  22317  cpnres  22318  ulmf2  22757  tglngne  23915  uhgraun  24289  umgraf  24296  vdgrfval  24873  eupai  24945  eupap1  24954  ghabloOLD  25349  fcoinver  27438  ofpreima  27485  ofpreima2  27486  fnct  27514  ofcfval  28075  probfinmeasb  28346  coinflipspace  28397  cvmtop1  28683  cvmtop2  28684  dfrdg2  29204  wfrlem3  29321  wfrlem4  29322  wfrlem9  29327  wfrlem12  29330  frrlem3  29365  frrlem4  29366  frrlem5e  29371  frrlem11  29375  imageval  29556  bpolylem  29786  filnetlem4  30175  sdclem2  30211  prdstotbnd  30266  heibor1lem  30281  ismrc  30609  dnnumch3lem  30968  dnnumch3  30969  aomclem4  30979  aomclem6  30981  fnchoice  31358  fnresdmss  31397  icccncfext  31644  stoweidlem35  31771  stoweidlem59  31795  fnresfnco  32165  fnbrafvb  32193  uhgun  32334  fnxpdmdm  32410  plusfreseq  32414  bnj564  33669  bnj945  33700  bnj545  33821  bnj548  33823  bnj570  33831  bnj900  33855  bnj929  33862  bnj983  33877  bnj1018  33888  bnj1110  33906  bnj1121  33909  bnj1145  33917  bnj1245  33938  bnj1253  33941  bnj1286  33943  bnj1280  33944  bnj1296  33945  bnj1311  33948  bnj1442  33973  bnj1450  33974  bnj1498  33985  bnj1514  33987  bnj1501  33991  diadm  36637  dibdiadm  36757  dibdmN  36759  dicdmN  36786  dihdm  36871
  Copyright terms: Public domain W3C validator