MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fndmi Structured version   Visualization version   GIF version

Theorem fndmi 6430
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
StepHypRef Expression
1 fndmi.1 . 2 𝐹 Fn 𝐴
2 fndm 6429 . 2 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
31, 2ax-mp 5 1 dom 𝐹 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  dom cdm 5523   Fn wfn 6323
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 210  df-an 400  df-fn 6331
This theorem is referenced by:  dmmpti  6468  dmmpo  7755  tfr2  8021  tz7.44-2  8030  rdgsuc  8047  tz7.48-2  8065  tz7.48-1  8066  tz7.48-3  8067  tz7.49  8068  brwitnlem  8119  om0x  8131  elpmi  8412  elmapex  8414  pmresg  8421  pmsspw  8428  r1suc  9187  r1ord  9197  r1ord3  9199  onwf  9247  r1val3  9255  r1pw  9262  rankr1b  9281  alephcard  9485  alephnbtwn  9486  alephgeom  9497  dfac12lem2  9559  alephsing  9691  hsmexlem6  9846  zorn2lem4  9914  alephadd  9992  alephreg  9997  pwcfsdom  9998  r1limwun  10151  r1wunlim  10152  rankcf  10192  inatsk  10193  r1tskina  10197  dmaddpi  10305  dmmulpi  10306  seqexw  13384  hashkf  13692  bpolylem  15398  0rest  16699  firest  16702  homfeqbas  16962  cidpropd  16976  2oppchomf  16990  fucbas  17226  fuchom  17227  xpccofval  17428  oppchofcl  17506  oyoncl  17516  mulgfval  18222  gicer  18412  psgneldm  18627  psgneldm2  18628  psgnval  18631  psgnghm  20273  psgnghm2  20274  cldrcl  21635  iscldtop  21704  restrcl  21766  ssrest  21785  resstopn  21795  hmpher  22393  nghmfval  23332  isnghm  23333  cvmtop1  32621  cvmtop2  32622  imageval  33505  filnetlem4  33843  ismrc  39639  dnnumch3lem  39987  dnnumch3  39988  aomclem4  39998  grur1cld  40937
  Copyright terms: Public domain W3C validator