Theorem fndm 6672

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5658  Fun wfun 6560   Fn wfn 6561

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 6569

This theorem is used by:  fndmi  6673  fndmd  6674  funfni  6675  fndmu  6676  fnbr  6677  fnunres1  6681  fncofn  6686  fnco  6687  fnresdm  6688  fnresdisj  6689  fnssresb  6691  fn0  6700  fnimadisj  6701  fnimaeq0  6702  f1odmOLD  6859  fvelimab  6988  fvun1  7007  eqfnfv2  7061  fndmdif  7072  fneqeql2  7077  elpreima  7088  elpreimaOLD  7089  fsn2  7169  fnsnbg  7201  fnprb  7245  fntpb  7246  fconst3  7250  fconst4  7251  fnfvima  7270  ralima  7274  fnunirn  7288  dff13  7289  nvof1o  7319  oprssov  7622  fnexALT  7997  curry1  8152  curry1val  8153  curry2  8155  curry2val  8157  fparlem3  8162  fparlem4  8163  offsplitfpar  8167  suppvalfng  8222  suppvalfn  8223  suppfnss  8244  fnsuppres  8246  tposfo2  8304  frrlem3  8344  frrlem4  8345  smodm2  8401  smoel2  8409  tfrlem8  8430  tfrlem9  8431  tfrlem9a  8432  tfrlem13  8436  tz7.44-3  8454  rdglim  8472  frsucmptn  8485  oaabs2  8696  omabs  8698  ixpprc  8985  undifixp  9000  bren  9021  fndmeng  9101  tfsnfin2  9390  inf0  9659  jech9.3OLD  9860  ssrankr1  9884  rankuni  9916  dfac3  10239  cfsmolem  10387  fin23lem31  10460  itunitc1  10537  ituniiun  10539  fnct  10659  fnctOLD  10660  cfpwsdom  10708  grur1  10944  genpdm  11126  fsuppmapnn0fiublem  14173  fsuppmapnn0fiub  14174  hashfn  14560  cshimadifsn  15022  cshimadifsn0  15023  shftfn  15269  rlimi2  15725  phimullem  17000  restsspw  17652  prdsdsval  17699  fnpr2ob  17780  sscpwex  18040  sscfn1  18042  sscfn2  18043  isssc  18045  funcres  18121  xpcbas  18402  xpchomfval  18403  gsumpropd2lem  18918  psgndmsubg  19767  dsmmbas2  22098  dsmmelbas  22100  islindf4  22199  restbas  23531  ptval  23944  kqcldsat  24107  kqnrmlem1  24117  kqnrmlem2  24118  hmphtop  24152  ustn0  24595  uniiccdif  25954  cpncn  26311  cpnres  26312  ulmf2  26768  tglngne  29070  uhgrn0  29702  upgrfn  29722  upgrex  29727  umgrfn  29734  fcoinver  33296  fresunsn  33317  nfpconfp  33324  opprabs  34110  mdetpmtr1  34566  coinflipspace  35224  bnj945  35515  bnj545  35636  bnj548  35638  bnj570  35646  bnj900  35670  bnj929  35677  bnj983  35692  bnj1018g  35704  bnj1018  35705  bnj1110  35723  bnj1145  35734  bnj1245  35755  bnj1253  35758  bnj1286  35760  bnj1280  35761  bnj1296  35762  bnj1311  35765  bnj1450  35791  bnj1498  35802  bnj1514  35804  bnj1501  35808  dfrdg2  36772  heibor1lem  39009  aks6d1c2lem4  43443  eqresfnbd  43553  aomclem6  44327  tfsconcatun  44600  tfsconcatb0  44607  tfsconcat0i  44608  tfsconcat0b  44609  tfsconcatrev  44611  tfsnfin  44615  ntrclsfv1  45316  ntrneifv1  45340  fnresdmss  46456  dmmptif  46551  fnresfnco  48384  fnfocofob  48422  fnbrafvb  48497  uniimaprimaeqfv  48737  elsetpreimafvssdm  48741  imasetpreimafvbijlemfo  48760  fnxpdmdm  49530  plusfreseq  49534  dmdm  50498