Theorem fndm 6647

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 6546	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
2	1	simprbi 503	1 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1569  dom cdm 5651  Fun wfun 6537   Fn wfn 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6546

This theorem is used by:  fndmi  6648  fndmd  6649  funfni  6650  fndmu  6651  fnbr  6652  fnunres1  6656  fncofn  6661  fnco  6662  fnresdm  6663  fnresdisj  6664  fnssresb  6666  fn0  6675  fnimadisj  6676  fnimaeq0  6677  f1odmOLD  6834  fvelimab  6962  fvun1  6981  eqfnfv2  7035  fndmdif  7046  fneqeql2  7051  elpreima  7062  fsn2  7142  fnsnbg  7174  fnprb  7218  fntpb  7219  fconst3  7223  fconst4  7224  fnfvima  7243  ralima  7247  fnunirn  7261  dff13  7262  nvof1o  7292  oprssov  7594  fnexALT  7967  curry1  8121  curry1val  8122  curry2  8124  curry2val  8126  fparlem3  8131  fparlem4  8132  offsplitfpar  8136  suppvalfng  8191  suppvalfn  8192  suppfnss  8213  fnsuppres  8215  tposfo2  8273  frrlem3  8313  frrlem4  8314  smodm2  8370  smoel2  8378  tfrlem8  8399  tfrlem9  8400  tfrlem9a  8401  tfrlem13  8405  tz7.44-3  8423  rdglim  8441  frsucmptn  8454  oaabs2  8665  omabs  8667  ixpprc  8954  undifixp  8969  bren  8990  fndmeng  9070  tfsnfin2  9359  inf0  9629  jech9.3OLD  9830  ssrankr1  9854  rankuni  9886  dfac3  10207  cfsmolem  10355  fin23lem31  10428  itunitc1  10505  ituniiun  10507  fnct  10627  fnctOLD  10628  cfpwsdom  10676  grur1  10912  genpdm  11094  fsuppmapnn0fiublem  14140  fsuppmapnn0fiub  14141  hashfn  14526  cshimadifsn  14988  cshimadifsn0  14989  shftfn  15235  rlimi2  15690  phimullem  16965  restsspw  17611  prdsdsval  17658  fnpr2ob  17739  sscpwex  17999  sscfn1  18001  sscfn2  18002  isssc  18004  funcres  18080  xpcbas  18361  xpchomfval  18362  gsumpropd2lem  18877  psgndmsubg  19725  dsmmbas2  22052  dsmmelbas  22054  islindf4  22153  restbas  23485  ptval  23898  kqcldsat  24061  kqnrmlem1  24071  kqnrmlem2  24072  hmphtop  24106  ustn0  24549  uniiccdif  25908  cpncn  26265  cpnres  26266  ulmf2  26720  tglngne  29022  uhgrn0  29654  upgrfn  29674  upgrex  29679  umgrfn  29686  fcoinver  33249  fresunsn  33270  nfpconfp  33277  opprabs  34056  mdetpmtr1  34505  coinflipspace  35163  bnj945  35454  bnj545  35575  bnj548  35577  bnj570  35585  bnj900  35609  bnj929  35616  bnj983  35631  bnj1018g  35643  bnj1018  35644  bnj1110  35662  bnj1145  35673  bnj1245  35694  bnj1253  35697  bnj1286  35699  bnj1280  35700  bnj1296  35701  bnj1311  35704  bnj1450  35730  bnj1498  35741  bnj1514  35743  bnj1501  35747  dfrdg2  36653  heibor1lem  38852  aks6d1c2lem4  43286  eqresfnbd  43395  aomclem6  44170  tfsconcatun  44448  tfsconcatb0  44455  tfsconcat0i  44456  tfsconcat0b  44457  tfsconcatrev  44459  tfsnfin  44463  ntrclsfv1  45164  ntrneifv1  45188  fnresdmss  46291  dmmptif  46386  fnresfnco  48219  fnfocofob  48257  fnbrafvb  48332  uniimaprimaeqfv  48572  elsetpreimafvssdm  48576  imasetpreimafvbijlemfo  48595  fnxpdmdm  49365  plusfreseq  49369  dmdm  50275