Theorem fndm 6584

Description: The domain of a function. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
fndm	⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)

Proof of Theorem fndm

Step	Hyp	Ref	Expression
1		df-fn 6484	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
2	1	simprbi 496	1 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5614  Fun wfun 6475   Fn wfn 6476

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 207  df-an 396  df-fn 6484

This theorem is referenced by:  fndmi  6585  fndmd  6586  funfni  6587  fndmu  6588  fnbr  6589  fnunres1  6593  fncofn  6598  fnco  6599  fnresdm  6600  fnresdisj  6601  fnssresb  6603  fn0  6612  fnimadisj  6613  fnimaeq0  6614  f1odm  6767  fvelimab  6894  fvun1  6913  eqfnfv2  6965  fndmdif  6975  fneqeql2  6980  elpreima  6991  fsn2  7069  fnsnbg  7098  fnprb  7142  fntpb  7143  fconst3  7147  fconst4  7148  fnfvima  7167  ralima  7171  fnunirn  7187  dff13  7188  nvof1o  7214  oprssov  7515  fnexALT  7883  curry1  8034  curry1val  8035  curry2  8037  curry2val  8039  fparlem3  8044  fparlem4  8045  offsplitfpar  8049  suppvalfng  8097  suppvalfn  8098  suppfnss  8119  fnsuppres  8121  tposfo2  8179  frrlem3  8218  frrlem4  8219  smodm2  8275  smoel2  8283  tfrlem8  8303  tfrlem9  8304  tfrlem9a  8305  tfrlem13  8309  tz7.44-3  8327  rdglim  8345  frsucmptn  8358  oaabs2  8564  omabs  8566  ixpprc  8843  undifixp  8858  bren  8879  fndmeng  8957  inf0  9511  r1lim  9665  jech9.3  9707  ssrankr1  9728  rankuni  9756  dfac3  10012  cfsmolem  10161  fin23lem31  10234  itunitc1  10311  ituniiun  10313  fnct  10428  cfpwsdom  10475  grur1  10711  genpdm  10893  fsuppmapnn0fiublem  13897  fsuppmapnn0fiub  13898  hashfn  14282  cshimadifsn  14736  cshimadifsn0  14737  shftfn  14980  rlimi2  15421  phimullem  16690  restsspw  17335  prdsdsval  17382  fnpr2ob  17462  sscpwex  17722  sscfn1  17724  sscfn2  17725  isssc  17727  funcres  17803  xpcbas  18084  xpchomfval  18085  gsumpropd2lem  18587  psgndmsubg  19414  dsmmbas2  21674  dsmmelbas  21676  islindf4  21775  restbas  23073  ptval  23485  kqcldsat  23648  kqnrmlem1  23658  kqnrmlem2  23659  hmphtop  23693  ustn0  24136  uniiccdif  25506  cpncn  25865  cpnres  25866  ulmf2  26320  tglngne  28528  uhgrn0  29045  upgrfn  29065  upgrex  29070  umgrfn  29077  fcoinver  32584  nfpconfp  32614  opprabs  33447  mdetpmtr1  33836  coinflipspace  34494  bnj945  34785  bnj545  34907  bnj548  34909  bnj570  34917  bnj900  34941  bnj929  34948  bnj983  34963  bnj1018g  34975  bnj1018  34976  bnj1110  34994  bnj1145  35005  bnj1245  35026  bnj1253  35029  bnj1286  35031  bnj1280  35032  bnj1296  35033  bnj1311  35036  bnj1450  35062  bnj1498  35073  bnj1514  35075  bnj1501  35079  dfrdg2  35837  heibor1lem  37857  aks6d1c2lem4  42168  eqresfnbd  42273  aomclem6  43100  tfsconcatun  43378  tfsconcatb0  43385  tfsconcat0i  43386  tfsconcat0b  43387  tfsconcatrev  43389  tfsnfin  43393  ntrclsfv1  44096  ntrneifv1  44120  fnresdmss  45213  dmmptif  45311  fnresfnco  47080  fnfocofob  47118  fnbrafvb  47193  uniimaprimaeqfv  47421  elsetpreimafvssdm  47425  imasetpreimafvbijlemfo  47444  fnxpdmdm  48199  plusfreseq  48203  dmdm  49093