![]() |
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 6514 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹:dom 𝐹⟶𝐵 ∧ dom 𝐹 ⊆ 𝐴)) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝜑 → (𝐹:dom 𝐹⟶𝐵 ∧ dom 𝐹 ⊆ 𝐴)) |
4 | 3 | simpld 499 | 1 ⊢ (𝜑 → 𝐹:dom 𝐹⟶𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 400 ⊆ wss 3854 dom cdm 5517 ⟶wf 6324 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-ext 2730 |
This theorem depends on definitions: df-bi 210 df-an 401 df-tru 1542 df-ex 1783 df-sb 2071 df-clab 2737 df-cleq 2751 df-clel 2831 df-v 3409 df-in 3861 df-ss 3871 df-fn 6331 df-f 6332 |
This theorem is referenced by: ordtypelem5 9004 ablfaclem2 19261 ablfac2 19264 f1lindf 20572 lmcnp 21989 upgr1e 26990 upgrres1 27187 umgrres1 27188 umgr2v2e 27399 pliguhgr 28353 s3f1 30730 ccatf1 30732 swrdf1 30737 tocyccntz 30922 dfac21 40368 xlimmnfvlem1 42825 xlimpnfvlem1 42829 itgperiod 42974 issmfd 43720 issmfdf 43722 cnfsmf 43725 issmfled 43742 issmfgtd 43745 smfsuplem1 43793 |
Copyright terms: Public domain | W3C validator |