![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ffdmd | Structured version Visualization version GIF version |
Description: The domain of a function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Ref | Expression |
---|---|
ffdmd.1 | ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
Ref | Expression |
---|---|
ffdmd | ⊢ (𝜑 → 𝐹:dom 𝐹⟶𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffdmd.1 | . . 3 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) | |
2 | ffdm 6734 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹:dom 𝐹⟶𝐵 ∧ dom 𝐹 ⊆ 𝐴)) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝜑 → (𝐹:dom 𝐹⟶𝐵 ∧ dom 𝐹 ⊆ 𝐴)) |
4 | 3 | simpld 495 | 1 ⊢ (𝜑 → 𝐹:dom 𝐹⟶𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ⊆ wss 3944 dom cdm 5669 ⟶wf 6528 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-v 3475 df-in 3951 df-ss 3961 df-fn 6535 df-f 6536 |
This theorem is referenced by: ordtypelem5 9499 ablfaclem2 19915 ablfac2 19918 f1lindf 21310 lmcnp 22737 upgr1e 28238 upgrres1 28435 umgrres1 28436 umgr2v2e 28647 pliguhgr 29602 s3f1 31984 ccatf1 31986 swrdf1 31991 tocyccntz 32174 dfac21 41579 xlimmnfvlem1 44321 xlimpnfvlem1 44325 itgperiod 44470 issmfd 45224 issmfdf 45226 cnfsmf 45229 issmfled 45246 issmfgtd 45250 smfsuplem1 45300 |
Copyright terms: Public domain | W3C validator |