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

Theorem fndm 6201
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 6104 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simprbi 486 1 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  dom cdm 5311  Fun wfun 6095   Fn wfn 6096
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 198  df-an 385  df-fn 6104
This theorem is referenced by:  funfni  6202  fndmu  6203  fnbr  6204  fnco  6210  fnresdm  6211  fnresdisj  6212  fnssresb  6214  fn0  6222  fnimadisj  6223  fnimaeq0  6224  dmmpti  6234  fdm  6264  f1dm  6320  f1odm  6357  f1o00  6387  fvelimab  6474  fvun1  6490  eqfnfv2  6534  fndmdif  6543  fneqeql2  6548  elpreima  6559  fsn2  6626  fnprb  6697  fntpb  6698  fconst3  6702  fconst4  6703  fnfvima  6721  fnunirn  6735  dff13  6736  nvof1o  6760  f1eqcocnv  6780  oprssov  7033  offval  7134  ofrfval  7135  fnexALT  7362  dmmpt2  7473  dmmpt2ga  7475  curry1  7503  curry1val  7504  curry2  7506  curry2val  7508  fparlem3  7513  fparlem4  7514  fnwelem  7526  suppvalfn  7536  suppfnss  7554  suppfnssOLD  7555  fnsuppres  7557  tposfo2  7610  wfrlem3  7651  wfrlem4  7653  wfrlem4OLD  7654  wfrdmcl  7659  wfrlem12  7662  wfrlem17  7667  smodm2  7688  smoel2  7696  tfrlem5  7712  tfrlem8  7716  tfrlem9  7717  tfrlem9a  7718  tfrlem13  7722  tfr2  7730  tz7.44-2  7739  tz7.44-3  7740  rdgsuc  7756  rdglim  7758  frsucmptn  7770  tz7.48-2  7773  tz7.48-1  7774  tz7.48-3  7775  tz7.49  7776  brwitnlem  7824  om0x  7836  oaabs2  7962  omabs  7964  elpmi  8111  elmapex  8113  pmresg  8120  pmsspw  8127  ixpprc  8166  undifixp  8181  bren  8201  fndmeng  8270  wemapso  8695  ixpiunwdom  8735  inf0  8765  r1suc  8880  r1lim  8882  r1ord  8890  r1ord3  8892  jech9.3  8924  onwf  8940  ssrankr1  8945  r1val3  8948  r1pw  8955  rankuni  8973  rankr1b  8974  alephcard  9176  alephnbtwn  9177  alephgeom  9188  dfac3  9227  dfac12lem1  9250  dfac12lem2  9251  cda1dif  9283  cdacomen  9288  cdadom1  9293  cdainf  9299  pwcdadom  9323  ackbij2lem3  9348  cfsmolem  9377  alephsing  9383  fin23lem31  9450  itunisuc  9526  itunitc1  9527  ituniiun  9529  hsmexlem6  9538  zorn2lem4  9606  ttukeylem3  9618  fnct  9644  alephadd  9684  alephreg  9689  pwcfsdom  9690  cfpwsdom  9691  r1limwun  9843  r1wunlim  9844  rankcf  9884  inatsk  9885  r1tskina  9889  grur1  9927  dmaddpi  9997  dmmulpi  9998  genpdm  10109  fsuppmapnn0fiublem  13013  fsuppmapnn0fiub  13014  hashkf  13339  hashfn  13382  wrdlndm  13532  cshimadifsn  13799  cshimadifsn0  13800  shftfn  14036  rlimi2  14468  bpolylem  14999  phimullem  15701  0rest  16295  restsspw  16297  firest  16298  prdsbas2  16334  prdsplusgval  16338  prdsmulrval  16340  prdsleval  16342  prdsdsval  16343  prdsvscaval  16344  imasleval  16406  xpsfrnel2  16430  homfeqbas  16560  cidpropd  16574  2oppchomf  16588  sscpwex  16679  sscfn1  16681  sscfn2  16682  ssclem  16683  isssc  16684  rescval2  16692  issubc2  16700  cofuval  16746  resfval2  16757  resf1st  16758  resf2nd  16759  funcres  16760  fucbas  16824  fuchom  16825  xpcbas  17023  xpchomfval  17024  xpccofval  17027  oppchofcl  17105  oyoncl  17115  gsumpropd2lem  17478  frmdss2  17605  gicer  17920  psgndmsubg  18123  psgneldm  18124  psgneldm2  18125  psgnval  18128  prdsmgp  18812  lspextmo  19263  psgnghm  20133  psgnghm2  20134  dsmmbas2  20291  dsmmfi  20292  dsmmelbas  20293  frlmsslsp  20345  islindf4  20387  ofco2  20468  cldrcl  21044  iscldtop  21113  neiss2  21119  restrcl  21175  restbas  21176  ssrest  21194  resstopn  21204  ptval  21587  txdis1cn  21652  qtopcld  21730  qtoprest  21734  kqsat  21748  kqdisj  21749  kqcldsat  21750  isr0  21754  kqnrmlem1  21760  kqnrmlem2  21761  hmphtop  21795  hmpher  21801  elfm3  21967  ustn0  22237  nghmfval  22739  isnghm  22740  ovolunlem1  23478  uniiccdif  23559  cpncn  23913  cpnres  23914  ulmf2  24352  tglngne  25659  uhgrn0  26176  upgrfn  26196  upgrex  26201  umgrfn  26208  fnunres1  29742  fcoinver  29743  ofpreima  29792  ofpreima2  29793  mdetpmtr1  30214  ofcfval  30485  probfinmeasb  30816  coinflipspace  30867  bnj564  31137  bnj945  31167  bnj545  31288  bnj548  31290  bnj570  31298  bnj900  31322  bnj929  31329  bnj983  31344  bnj1018  31355  bnj1110  31373  bnj1121  31376  bnj1145  31384  bnj1245  31405  bnj1253  31408  bnj1286  31410  bnj1280  31411  bnj1296  31412  bnj1311  31415  bnj1442  31440  bnj1450  31441  bnj1498  31452  bnj1514  31454  bnj1501  31458  cvmtop1  31565  cvmtop2  31566  dfrdg2  32021  frrlem3  32103  frrlem4  32104  frrlem5e  32109  frrlem11  32113  imageval  32358  filnetlem4  32697  sdclem2  33849  prdstotbnd  33904  heibor1lem  33919  diadm  36816  dibdiadm  36936  dibdmN  36938  dicdmN  36965  dihdm  37050  ismrc  37766  dnnumch3lem  38117  dnnumch3  38118  aomclem4  38128  aomclem6  38130  ntrclsfv1  38853  ntrneifv1  38877  fnchoice  39682  fnresdmss  39837  wessf1ornlem  39860  fndmd  39925  icccncfext  40580  stoweidlem35  40731  stoweidlem59  40755  fnresfnco  41660  fnbrafvb  41743  fnxpdmdm  42336  plusfreseq  42340
  Copyright terms: Public domain W3C validator