Theorem fndm 6454

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

Syntax hints:   → wi 4   = wceq 1533  dom cdm 5554  Fun wfun 6348   Fn wfn 6349

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 209  df-an 399  df-fn 6357

This theorem is referenced by:  fndmd  6455  funfni  6456  fndmu  6457  fnbr  6458  fnco  6464  fnresdm  6465  fnresdisj  6466  fnssresb  6468  fn0  6478  fnimadisj  6479  fnimaeq0  6480  dmmpti  6491  fdm  6521  f1dm  6578  f1odm  6618  fvelimab  6736  fvun1  6753  eqfnfv2  6802  fndmdif  6811  fneqeql2  6816  elpreima  6827  fsn2  6897  fnprb  6970  fntpb  6971  fconst3  6975  fconst4  6976  fnfvima  6994  fnunirn  7011  dff13  7012  nvof1o  7036  f1eqcocnv  7056  oprssov  7316  fnexALT  7651  dmmpo  7768  dmmpoga  7770  curry1  7798  curry1val  7799  curry2  7801  curry2val  7803  fparlem3  7808  fparlem4  7809  offsplitfpar  7814  fnwelem  7824  suppvalfn  7836  suppfnss  7854  fnsuppres  7856  tposfo2  7914  wfrlem3  7955  wfrlem4  7957  wfrdmcl  7962  wfrlem12  7965  wfrlem17  7970  smodm2  7991  smoel2  7999  tfrlem5  8015  tfrlem8  8019  tfrlem9  8020  tfrlem9a  8021  tfrlem13  8025  tfr2  8033  tz7.44-2  8042  tz7.44-3  8043  rdgsuc  8059  rdglim  8061  frsucmptn  8073  tz7.48-2  8077  tz7.48-1  8078  tz7.48-3  8079  tz7.49  8080  brwitnlem  8131  om0x  8143  oaabs2  8271  omabs  8273  elpmi  8424  elmapex  8426  pmresg  8433  pmsspw  8440  ixpprc  8482  undifixp  8497  bren  8517  fndmeng  8586  ixpiunwdom  9054  inf0  9083  r1suc  9198  r1lim  9200  r1ord  9208  r1ord3  9210  jech9.3  9242  onwf  9258  ssrankr1  9263  r1val3  9266  r1pw  9273  rankuni  9291  rankr1b  9292  alephcard  9495  alephnbtwn  9496  alephgeom  9507  dfac3  9546  dfac12lem1  9568  dfac12lem2  9569  ackbij2lem3  9662  cfsmolem  9691  alephsing  9697  fin23lem31  9764  itunisuc  9840  itunitc1  9841  ituniiun  9843  hsmexlem6  9852  zorn2lem4  9920  ttukeylem3  9932  fnct  9958  alephadd  9998  alephreg  10003  pwcfsdom  10004  cfpwsdom  10005  r1limwun  10157  r1wunlim  10158  rankcf  10198  inatsk  10199  r1tskina  10203  grur1  10241  dmaddpi  10311  dmmulpi  10312  genpdm  10423  fsuppmapnn0fiublem  13357  fsuppmapnn0fiub  13358  seqexw  13384  hashkf  13691  hashfn  13735  wrdlndmOLD  13879  cshimadifsn  14190  cshimadifsn0  14191  shftfn  14431  rlimi2  14870  bpolylem  15401  phimullem  16115  0rest  16702  restsspw  16704  firest  16705  prdsbas2  16741  prdsplusgval  16745  prdsmulrval  16747  prdsleval  16749  prdsdsval  16750  prdsvscaval  16751  imasleval  16813  fnpr2ob  16830  homfeqbas  16965  cidpropd  16979  2oppchomf  16993  sscpwex  17084  sscfn1  17086  sscfn2  17087  ssclem  17088  isssc  17089  rescval2  17097  issubc2  17105  cofuval  17151  resfval2  17162  resf1st  17163  resf2nd  17164  funcres  17165  fucbas  17229  fuchom  17230  xpcbas  17427  xpchomfval  17428  xpccofval  17431  oppchofcl  17509  oyoncl  17519  gsumpropd2lem  17888  mulgfval  18225  gicer  18415  psgndmsubg  18629  psgneldm  18630  psgneldm2  18631  psgnval  18634  prdsmgp  19359  lspextmo  19827  psgnghm  20723  psgnghm2  20724  dsmmbas2  20880  dsmmfi  20881  dsmmelbas  20882  islindf4  20981  ofco2  21059  cldrcl  21633  iscldtop  21702  neiss2  21708  restrcl  21764  restbas  21765  ssrest  21783  resstopn  21793  ptval  22177  txdis1cn  22242  qtopcld  22320  qtoprest  22324  kqsat  22338  kqdisj  22339  kqcldsat  22340  isr0  22344  kqnrmlem1  22350  kqnrmlem2  22351  hmphtop  22385  hmpher  22391  elfm3  22557  ustn0  22828  nghmfval  23330  isnghm  23331  ovolunlem1  24097  uniiccdif  24178  cpncn  24532  cpnres  24533  ulmf2  24971  tglngne  26335  uhgrn0  26851  upgrfn  26871  upgrex  26876  umgrfn  26883  fnunres1  30355  fcoinver  30356  nfpconfp  30376  ofpreima  30409  ofpreima2  30410  fnpreimac  30415  mdetpmtr1  31088  probfinmeasb  31686  coinflipspace  31738  bnj564  32015  bnj945  32045  bnj545  32167  bnj548  32169  bnj570  32177  bnj900  32201  bnj929  32208  bnj983  32223  bnj1018g  32235  bnj1018  32236  bnj1110  32254  bnj1145  32265  bnj1245  32286  bnj1253  32289  bnj1286  32291  bnj1280  32292  bnj1296  32293  bnj1311  32296  bnj1442  32321  bnj1450  32322  bnj1498  32333  bnj1514  32335  bnj1501  32339  cvmtop1  32507  cvmtop2  32508  dfrdg2  33040  frrlem3  33125  frrlem4  33126  frrlem8  33130  frrlem10  33132  imageval  33391  filnetlem4  33729  sdclem2  35016  prdstotbnd  35071  heibor1lem  35086  dibdiadm  38290  dibdmN  38292  dicdmN  38319  dihdm  38404  fnsnbt  39118  ismrc  39296  dnnumch3lem  39644  dnnumch3  39645  aomclem4  39655  aomclem6  39657  ntrclsfv1  40403  ntrneifv1  40427  grur1cld  40566  fnresdmss  41422  icccncfext  42168  stoweidlem35  42319  stoweidlem59  42343  fnresfnco  43275  fnbrafvb  43352  uniimaprimaeqfv  43541  elsetpreimafvssdm  43545  imasetpreimafvbijlemfo  43564  fnxpdmdm  44034  plusfreseq  44038