Theorem fndmi 6668

Description: The domain of a function. (Contributed by Wolf Lammen, 1-Jun-2024.)

Hypothesis

Ref	Expression
fndmi.1	⊢ 𝐹 Fn 𝐴

Assertion

Ref	Expression
fndmi	⊢ dom 𝐹 = 𝐴

Proof of Theorem fndmi

Step	Hyp	Ref	Expression
1		fndmi.1	. 2 ⊢ 𝐹 Fn 𝐴
2		fndm 6667	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ dom 𝐹 = 𝐴

This proof depends on syntax axioms:   = wceq 1570  dom cdm 5656   Fn wfn 6556

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 6564

This theorem is used by:  dmmpti  6708  dmmpo  8110  tfr2  8437  tz7.44-2  8446  rdgsuc  8463  tz7.48-2  8483  tz7.48-1  8484  tz7.48-3  8485  tz7.49  8486  brwitnlem  8546  om0x  8558  naddcllem  8716  naddov2  8719  naddasslem1  8735  naddasslem2  8736  elpmi  8897  elmapex  8899  pmresg  8929  pmsspw  8936  r1suc  9807  r1lim  9809  r1ord  9817  r1ord3  9819  onwf  9870  r1wf  9871  r1val3  9880  r1pw  9889  rankr1b  9911  alephcard  10179  alephnbtwn  10180  alephgeom  10191  dfac12lem2  10253  alephsing  10384  hsmexlem6  10539  zorn2lem4  10607  alephadd  10692  alephreg  10697  pwcfsdom  10698  r1limwun  10851  r1wunlim  10852  rankcf  10892  inatsk  10893  r1tskina  10897  dmaddpi  11005  dmmulpi  11006  seqexw  14190  hashkf  14506  bpolylem  16246  0rest  17632  firest  17635  homfeqbas  17902  cidpropd  17916  2oppchomf  17930  fucbas  18170  fuchom  18171  xpccofval  18388  oppchofcl  18466  oyoncl  18476  ex-chn2  18844  mulgfval  19311  gicer  19524  psgneldm  19750  psgneldm2  19751  psgnval  19754  ricrel  20777  psgnghm  21919  psgnghm2  21920  cldrcl  23377  iscldtop  23446  restrcl  23508  ssrest  23527  resstopn  23537  hmpher  24136  nghmfval  25074  isnghm  25075  bdaydm  28168  newval  28254  negsproplem2  28448  onrankid  35824  rankfo  35830  acwer1prclem  35864  acwer1prc  35865  j0ltaleph  36021  jltaleph  36039  fnlfvk30  36040  fnlfvk3n0  36041  cvmtop1  36205  cvmtop2  36206  imageval  36883  rankeq1o  37123  hfninf  37126  filnetlem4  37360  ismrc  43916  dnnumch3lem  44257  dnnumch3  44258  aomclem4  44263  grur1cld  45433  gricrel  49232  grlicrel  49319  fonex  50193  cicrcl2  50372  cic1st2nd  50376  oppfrcl  50459  eloppf  50464  initopropdlemlem  50576  initopropd  50580  termopropd  50581  zeroopropd  50582  reldmxpc  50583  reldmlan2  51015  reldmran2  51016  lanrcl  51019  ranrcl  51020