Theorem fndm 6449

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

Syntax hints:   → wi 4   = wceq 1533  dom cdm 5549  Fun wfun 6343   Fn wfn 6344

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 6352

This theorem is referenced by:  fndmd  6450  funfni  6451  fndmu  6452  fnbr  6453  fnco  6459  fnresdm  6460  fnresdisj  6461  fnssresb  6463  fn0  6473  fnimadisj  6474  fnimaeq0  6475  dmmpti  6486  fdm  6516  f1dm  6573  f1odm  6613  fvelimab  6731  fvun1  6748  eqfnfv2  6797  fndmdif  6806  fneqeql2  6811  elpreima  6822  fsn2  6892  fnprb  6965  fntpb  6966  fconst3  6970  fconst4  6971  fnfvima  6989  fnunirn  7006  dff13  7007  nvof1o  7031  f1eqcocnv  7051  oprssov  7311  fnexALT  7646  dmmpo  7763  dmmpoga  7765  curry1  7793  curry1val  7794  curry2  7796  curry2val  7798  fparlem3  7803  fparlem4  7804  offsplitfpar  7809  fnwelem  7819  suppvalfn  7831  suppfnss  7849  fnsuppres  7851  tposfo2  7909  wfrlem3  7950  wfrlem4  7952  wfrdmcl  7957  wfrlem12  7960  wfrlem17  7965  smodm2  7986  smoel2  7994  tfrlem5  8010  tfrlem8  8014  tfrlem9  8015  tfrlem9a  8016  tfrlem13  8020  tfr2  8028  tz7.44-2  8037  tz7.44-3  8038  rdgsuc  8054  rdglim  8056  frsucmptn  8068  tz7.48-2  8072  tz7.48-1  8073  tz7.48-3  8074  tz7.49  8075  brwitnlem  8126  om0x  8138  oaabs2  8266  omabs  8268  elpmi  8419  elmapex  8421  pmresg  8428  pmsspw  8435  ixpprc  8477  undifixp  8492  bren  8512  fndmeng  8581  ixpiunwdom  9049  inf0  9078  r1suc  9193  r1lim  9195  r1ord  9203  r1ord3  9205  jech9.3  9237  onwf  9253  ssrankr1  9258  r1val3  9261  r1pw  9268  rankuni  9286  rankr1b  9287  alephcard  9490  alephnbtwn  9491  alephgeom  9502  dfac3  9541  dfac12lem1  9563  dfac12lem2  9564  ackbij2lem3  9657  cfsmolem  9686  alephsing  9692  fin23lem31  9759  itunisuc  9835  itunitc1  9836  ituniiun  9838  hsmexlem6  9847  zorn2lem4  9915  ttukeylem3  9927  fnct  9953  alephadd  9993  alephreg  9998  pwcfsdom  9999  cfpwsdom  10000  r1limwun  10152  r1wunlim  10153  rankcf  10193  inatsk  10194  r1tskina  10198  grur1  10236  dmaddpi  10306  dmmulpi  10307  genpdm  10418  fsuppmapnn0fiublem  13352  fsuppmapnn0fiub  13353  seqexw  13379  hashkf  13686  hashfn  13730  wrdlndmOLD  13874  cshimadifsn  14185  cshimadifsn0  14186  shftfn  14426  rlimi2  14865  bpolylem  15396  phimullem  16110  0rest  16697  restsspw  16699  firest  16700  prdsbas2  16736  prdsplusgval  16740  prdsmulrval  16742  prdsleval  16744  prdsdsval  16745  prdsvscaval  16746  imasleval  16808  fnpr2ob  16825  homfeqbas  16960  cidpropd  16974  2oppchomf  16988  sscpwex  17079  sscfn1  17081  sscfn2  17082  ssclem  17083  isssc  17084  rescval2  17092  issubc2  17100  cofuval  17146  resfval2  17157  resf1st  17158  resf2nd  17159  funcres  17160  fucbas  17224  fuchom  17225  xpcbas  17422  xpchomfval  17423  xpccofval  17426  oppchofcl  17504  oyoncl  17514  gsumpropd2lem  17883  mulgfval  18220  gicer  18410  psgndmsubg  18624  psgneldm  18625  psgneldm2  18626  psgnval  18629  prdsmgp  19354  lspextmo  19822  psgnghm  20718  psgnghm2  20719  dsmmbas2  20875  dsmmfi  20876  dsmmelbas  20877  islindf4  20976  ofco2  21054  cldrcl  21628  iscldtop  21697  neiss2  21703  restrcl  21759  restbas  21760  ssrest  21778  resstopn  21788  ptval  22172  txdis1cn  22237  qtopcld  22315  qtoprest  22319  kqsat  22333  kqdisj  22334  kqcldsat  22335  isr0  22339  kqnrmlem1  22345  kqnrmlem2  22346  hmphtop  22380  hmpher  22386  elfm3  22552  ustn0  22823  nghmfval  23325  isnghm  23326  ovolunlem1  24092  uniiccdif  24173  cpncn  24527  cpnres  24528  ulmf2  24966  tglngne  26330  uhgrn0  26846  upgrfn  26866  upgrex  26871  umgrfn  26878  fnunres1  30350  fcoinver  30351  nfpconfp  30371  ofpreima  30404  ofpreima2  30405  fnpreimac  30410  mdetpmtr1  31083  probfinmeasb  31681  coinflipspace  31733  bnj564  32010  bnj945  32040  bnj545  32162  bnj548  32164  bnj570  32172  bnj900  32196  bnj929  32203  bnj983  32218  bnj1018g  32230  bnj1018  32231  bnj1110  32249  bnj1145  32260  bnj1245  32281  bnj1253  32284  bnj1286  32286  bnj1280  32287  bnj1296  32288  bnj1311  32291  bnj1442  32316  bnj1450  32317  bnj1498  32328  bnj1514  32330  bnj1501  32334  cvmtop1  32502  cvmtop2  32503  dfrdg2  33035  frrlem3  33120  frrlem4  33121  frrlem8  33125  frrlem10  33127  imageval  33386  filnetlem4  33724  sdclem2  35011  prdstotbnd  35066  heibor1lem  35081  dibdiadm  38285  dibdmN  38287  dicdmN  38314  dihdm  38399  fnsnbt  39113  ismrc  39291  dnnumch3lem  39639  dnnumch3  39640  aomclem4  39650  aomclem6  39652  ntrclsfv1  40398  ntrneifv1  40422  grur1cld  40561  fnresdmss  41417  icccncfext  42163  stoweidlem35  42314  stoweidlem59  42338  fnresfnco  43270  fnbrafvb  43347  uniimaprimaeqfv  43536  elsetpreimafvssdm  43540  imasetpreimafvbijlemfo  43559  fnxpdmdm  44029  plusfreseq  44033