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

Theorem fndm 5958
Description: The domain of a function. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fndm (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)

Proof of Theorem fndm
StepHypRef Expression
1 df-fn 5860 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simprbi 480 1 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  dom cdm 5084  Fun wfun 5851   Fn wfn 5852
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 197  df-an 386  df-fn 5860
This theorem is referenced by:  funfni  5959  fndmu  5960  fnbr  5961  fnco  5967  fnresdm  5968  fnresdisj  5969  fnssresb  5971  fn0  5978  fnimadisj  5979  fnimaeq0  5980  dmmpti  5990  fdm  6018  f1dm  6072  f1odm  6108  f1o00  6138  fvelimab  6220  fvun1  6236  eqfnfv2  6278  fndmdif  6287  fneqeql2  6292  elpreima  6303  fsn2  6368  fnprb  6437  fntpb  6438  fconst3  6442  fconst4  6443  fnfvima  6461  fnunirn  6476  dff13  6477  nvof1o  6501  f1eqcocnv  6521  oprssov  6768  offval  6869  ofrfval  6870  fnexALT  7094  dmmpt2  7200  dmmpt2ga  7202  curry1  7229  curry1val  7230  curry2  7232  curry2val  7234  fparlem3  7239  fparlem4  7240  fnwelem  7252  suppvalfn  7262  suppfnss  7280  fnsuppres  7282  tposfo2  7335  wfrlem3  7376  wfrlem4  7378  wfrdmcl  7383  wfrlem12  7386  wfrlem17  7391  smodm2  7412  smoel2  7420  tfrlem5  7436  tfrlem8  7440  tfrlem9  7441  tfrlem9a  7442  tfrlem13  7446  tfr2  7454  tz7.44-2  7463  tz7.44-3  7464  rdgsuc  7480  rdglim  7482  frsucmptn  7494  tz7.48-2  7497  tz7.48-1  7498  tz7.48-3  7499  tz7.49  7500  brwitnlem  7547  om0x  7559  oaabs2  7685  omabs  7687  elpmi  7836  elmapex  7838  pmresg  7845  pmsspw  7852  ixpprc  7889  undifixp  7904  bren  7924  fndmeng  7994  wemapso  8416  ixpiunwdom  8456  inf0  8478  r1suc  8593  r1lim  8595  r1ord  8603  r1ord3  8605  jech9.3  8637  onwf  8653  ssrankr1  8658  r1val3  8661  r1pw  8668  rankuni  8686  rankr1b  8687  alephcard  8853  alephnbtwn  8854  alephgeom  8865  dfac3  8904  dfac12lem1  8925  dfac12lem2  8926  cda1dif  8958  cdacomen  8963  cdadom1  8968  cdainf  8974  pwcdadom  8998  ackbij2lem3  9023  cfsmolem  9052  alephsing  9058  fin23lem31  9125  itunisuc  9201  itunitc1  9202  ituniiun  9204  hsmexlem6  9213  zorn2lem4  9281  ttukeylem3  9293  fnct  9319  alephadd  9359  alephreg  9364  pwcfsdom  9365  cfpwsdom  9366  r1limwun  9518  r1wunlim  9519  rankcf  9559  inatsk  9560  r1tskina  9564  grur1  9602  dmaddpi  9672  dmmulpi  9673  genpdm  9784  fsuppmapnn0fiublem  12745  fsuppmapnn0fiub  12746  fsuppmapnn0fiubOLD  12747  hashkf  13075  hashfn  13120  wrdlndm  13276  cshimadifsn  13528  cshimadifsn0  13529  shftfn  13763  rlimi2  14195  bpolylem  14723  phimullem  15427  0rest  16030  restsspw  16032  firest  16033  prdsbas2  16069  prdsplusgval  16073  prdsmulrval  16075  prdsleval  16077  prdsdsval  16078  prdsvscaval  16079  imasleval  16141  xpsfrnel2  16165  homfeqbas  16296  cidpropd  16310  2oppchomf  16324  sscpwex  16415  sscfn1  16417  sscfn2  16418  ssclem  16419  isssc  16420  rescval2  16428  issubc2  16436  cofuval  16482  resfval2  16493  resf1st  16494  resf2nd  16495  funcres  16496  fucbas  16560  fuchom  16561  xpcbas  16758  xpchomfval  16759  xpccofval  16762  oppchofcl  16840  oyoncl  16850  gsumpropd2lem  17213  frmdss2  17340  gicer  17658  gicerOLD  17659  psgndmsubg  17862  psgneldm  17863  psgneldm2  17864  psgnval  17867  prdsmgp  18550  lspextmo  18996  psgnghm  19866  psgnghm2  19867  dsmmbas2  20021  dsmmfi  20022  dsmmelbas  20023  frlmsslsp  20075  islindf4  20117  ofco2  20197  cldrcl  20770  iscldtop  20839  neiss2  20845  restrcl  20901  restbas  20902  ssrest  20920  resstopn  20930  ptval  21313  txdis1cn  21378  qtopcld  21456  qtoprest  21460  kqsat  21474  kqdisj  21475  kqcldsat  21476  isr0  21480  kqnrmlem1  21486  kqnrmlem2  21487  hmphtop  21521  hmpher  21527  elfm3  21694  ustn0  21964  nghmfval  22466  isnghm  22467  ovolunlem1  23205  uniiccdif  23286  cpncn  23639  cpnres  23640  ulmf2  24076  tglngne  25379  uhgrn0  25892  upgrfn  25912  upgrex  25917  umgrfn  25923  fcoinver  29302  ofpreima  29349  ofpreima2  29350  mdetpmtr1  29713  ofcfval  29983  probfinmeasb  30314  coinflipspace  30365  bnj564  30575  bnj945  30605  bnj545  30726  bnj548  30728  bnj570  30736  bnj900  30760  bnj929  30767  bnj983  30782  bnj1018  30793  bnj1110  30811  bnj1121  30814  bnj1145  30822  bnj1245  30843  bnj1253  30846  bnj1286  30848  bnj1280  30849  bnj1296  30850  bnj1311  30853  bnj1442  30878  bnj1450  30879  bnj1498  30890  bnj1514  30892  bnj1501  30896  cvmtop1  31003  cvmtop2  31004  dfrdg2  31455  frrlem3  31536  frrlem4  31537  frrlem5e  31542  frrlem11  31546  imageval  31732  filnetlem4  32071  sdclem2  33209  prdstotbnd  33264  heibor1lem  33279  diadm  35843  dibdiadm  35963  dibdmN  35965  dicdmN  35992  dihdm  36077  ismrc  36783  dnnumch3lem  37135  dnnumch3  37136  aomclem4  37146  aomclem6  37148  ntrclsfv1  37874  ntrneifv1  37898  fnchoice  38710  fnresdmss  38857  wessf1ornlem  38880  fndmd  38951  icccncfext  39435  stoweidlem35  39589  stoweidlem59  39613  fnresfnco  40540  fnbrafvb  40568  fnxpdmdm  41086  plusfreseq  41090
  Copyright terms: Public domain W3C validator