![]() |
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 6429 | . 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ dom 𝐹 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 dom cdm 5517 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 401 df-fn 6331 |
This theorem is referenced by: dmmpti 6468 dmmpo 7766 tfr2 8037 tz7.44-2 8046 rdgsuc 8063 tz7.48-2 8081 tz7.48-1 8082 tz7.48-3 8083 tz7.49 8084 brwitnlem 8135 om0x 8147 elpmi 8428 elmapex 8430 pmresg 8445 pmsspw 8452 r1suc 9217 r1ord 9227 r1ord3 9229 onwf 9277 r1val3 9285 r1pw 9292 rankr1b 9311 alephcard 9515 alephnbtwn 9516 alephgeom 9527 dfac12lem2 9589 alephsing 9721 hsmexlem6 9876 zorn2lem4 9944 alephadd 10022 alephreg 10027 pwcfsdom 10028 r1limwun 10181 r1wunlim 10182 rankcf 10222 inatsk 10223 r1tskina 10227 dmaddpi 10335 dmmulpi 10336 seqexw 13419 hashkf 13727 bpolylem 15435 0rest 16746 firest 16749 homfeqbas 17009 cidpropd 17023 2oppchomf 17037 fucbas 17274 fuchom 17275 xpccofval 17483 oppchofcl 17561 oyoncl 17571 mulgfval 18278 gicer 18468 psgneldm 18683 psgneldm2 18684 psgnval 18687 psgnghm 20330 psgnghm2 20331 cldrcl 21711 iscldtop 21780 restrcl 21842 ssrest 21861 resstopn 21871 hmpher 22469 nghmfval 23409 isnghm 23410 cvmtop1 32723 cvmtop2 32724 imageval 33766 filnetlem4 34104 ismrc 40000 dnnumch3lem 40348 dnnumch3 40349 aomclem4 40359 grur1cld 41298 |
Copyright terms: Public domain | W3C validator |