| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > fndmi | Structured version Visualization version GIF version | ||
| Description: The domain of a function. (Contributed by Wolf Lammen, 1-Jun-2024.) |
| Ref | Expression |
|---|---|
| fndmi.1 | ⊢ 𝐹 Fn 𝐴 |
| Ref | Expression |
|---|---|
| fndmi | ⊢ dom 𝐹 = 𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fndmi.1 | . 2 ⊢ 𝐹 Fn 𝐴 | |
| 2 | fndm 6671 | . 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ dom 𝐹 = 𝐴 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 dom cdm 5685 Fn wfn 6556 |
| 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 6564 |
| This theorem is referenced by: dmmpti 6712 dmmpo 8096 tfr2 8438 tz7.44-2 8447 rdgsuc 8464 tz7.48-2 8482 tz7.48-1 8483 tz7.48-3 8484 tz7.49 8485 brwitnlem 8545 om0x 8557 naddcllem 8714 naddov2 8717 naddasslem1 8732 naddasslem2 8733 elpmi 8886 elmapex 8888 pmresg 8910 pmsspw 8917 r1suc 9810 r1ord 9820 r1ord3 9822 onwf 9870 r1val3 9878 r1pw 9885 rankr1b 9904 alephcard 10110 alephnbtwn 10111 alephgeom 10122 dfac12lem2 10185 alephsing 10316 hsmexlem6 10471 zorn2lem4 10539 alephadd 10617 alephreg 10622 pwcfsdom 10623 r1limwun 10776 r1wunlim 10777 rankcf 10817 inatsk 10818 r1tskina 10822 dmaddpi 10930 dmmulpi 10931 seqexw 14058 hashkf 14371 bpolylem 16084 0rest 17474 firest 17477 homfeqbas 17739 cidpropd 17753 2oppchomf 17767 fucbas 18008 fuchom 18009 xpccofval 18227 oppchofcl 18305 oyoncl 18315 mulgfval 19087 gicer 19295 psgneldm 19521 psgneldm2 19522 psgnval 19525 psgnghm 21598 psgnghm2 21599 cldrcl 23034 iscldtop 23103 restrcl 23165 ssrest 23184 resstopn 23194 hmpher 23792 nghmfval 24743 isnghm 24744 newval 27894 negsproplem2 28061 cvmtop1 35265 cvmtop2 35266 imageval 35931 filnetlem4 36382 ismrc 42712 dnnumch3lem 43058 dnnumch3 43059 aomclem4 43069 grur1cld 44251 gricrel 47888 grlicrel 47966 reldmxpc 48952 |
| Copyright terms: Public domain | W3C validator |