Theorem fndmi 6596

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 6595	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ dom 𝐹 = 𝐴

Syntax hints:   = wceq 1542  dom cdm 5624   Fn wfn 6487

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 207  df-an 396  df-fn 6495

This theorem is referenced by:  dmmpti  6636  dmmpo  8017  tfr2  8330  tz7.44-2  8339  rdgsuc  8356  tz7.48-2  8374  tz7.48-1  8375  tz7.48-3  8376  tz7.49  8377  brwitnlem  8435  om0x  8447  naddcllem  8605  naddov2  8608  naddasslem1  8623  naddasslem2  8624  elpmi  8786  elmapex  8788  pmresg  8811  pmsspw  8818  r1suc  9685  r1ord  9695  r1ord3  9697  onwf  9745  r1val3  9753  r1pw  9760  rankr1b  9779  alephcard  9983  alephnbtwn  9984  alephgeom  9995  dfac12lem2  10058  alephsing  10189  hsmexlem6  10344  zorn2lem4  10412  alephadd  10491  alephreg  10496  pwcfsdom  10497  r1limwun  10650  r1wunlim  10651  rankcf  10691  inatsk  10692  r1tskina  10696  dmaddpi  10804  dmmulpi  10805  seqexw  13970  hashkf  14285  bpolylem  16004  0rest  17383  firest  17386  homfeqbas  17653  cidpropd  17667  2oppchomf  17681  fucbas  17921  fuchom  17922  xpccofval  18139  oppchofcl  18217  oyoncl  18227  ex-chn2  18595  mulgfval  19036  gicer  19243  psgneldm  19469  psgneldm2  19470  psgnval  19473  psgnghm  21570  psgnghm2  21571  cldrcl  23001  iscldtop  23070  restrcl  23132  ssrest  23151  resstopn  23161  hmpher  23759  nghmfval  24697  isnghm  24698  newval  27841  negsproplem2  28035  r1wf  35255  r1elcl  35257  cvmtop1  35458  cvmtop2  35459  imageval  36126  filnetlem4  36579  ismrc  43147  dnnumch3lem  43492  dnnumch3  43493  aomclem4  43503  grur1cld  44677  gricrel  48407  grlicrel  48494  fonex  49354  cicrcl2  49530  cic1st2nd  49534  oppfrcl  49615  eloppf  49620  initopropdlemlem  49726  initopropd  49730  termopropd  49731  zeroopropd  49732  reldmxpc  49733  reldmlan2  50104  reldmran2  50105  lanrcl  50108  ranrcl  50109