![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fssdm | Structured version Visualization version GIF version |
Description: Expressing that a class is a subclass of the domain of a function expressed in maps-to notation, semi-deduction form. (Contributed by AV, 21-Aug-2022.) |
Ref | Expression |
---|---|
fssdm.d | ⊢ 𝐷 ⊆ dom 𝐹 |
fssdm.f | ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
Ref | Expression |
---|---|
fssdm | ⊢ (𝜑 → 𝐷 ⊆ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fssdm.d | . 2 ⊢ 𝐷 ⊆ dom 𝐹 | |
2 | fssdm.f | . . 3 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) | |
3 | 2 | fdmd 6347 | . 2 ⊢ (𝜑 → dom 𝐹 = 𝐴) |
4 | 1, 3 | syl5sseq 3905 | 1 ⊢ (𝜑 → 𝐷 ⊆ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3825 dom cdm 5400 ⟶wf 6178 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-ext 2745 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-clab 2754 df-cleq 2765 df-clel 2840 df-in 3832 df-ss 3839 df-fn 6185 df-f 6186 |
This theorem is referenced by: fisuppfi 8628 wemapso 8802 wemapso2lem 8803 cantnfcl 8916 cantnfle 8920 cantnflt 8921 cantnff 8923 cantnfp1lem3 8929 cantnflem1b 8935 cantnflem1 8938 cantnflem3 8940 cnfcomlem 8948 cnfcom 8949 cnfcom3lem 8952 cnfcom3 8953 fin1a2lem7 9618 isercolllem2 14873 isercolllem3 14874 fsumss 14932 fprodss 15152 vdwlem1 16163 vdwlem5 16167 vdwlem6 16168 ghmpreima 18141 pmtrfconj 18345 gsumval3lem1 18769 gsumval3lem2 18770 gsumval3 18771 gsumzres 18773 gsumzcl2 18774 gsumzf1o 18776 gsumzmhm 18800 gsumzoppg 18807 gsum2d 18835 dpjidcl 18920 lmhmpreima 19532 mplcoe1 19949 mplcoe5 19952 psr1baslem 20046 gsumfsum 20304 regsumsupp 20458 frlmlbs 20633 mdetdiaglem 20901 cnclima 21570 iscncl 21571 cnclsi 21574 txcnmpt 21926 qtopval2 21998 qtopcn 22016 rnelfmlem 22254 fmfnfmlem4 22259 clssubg 22410 tgphaus 22418 tsmsgsum 22440 xmeter 22736 metustss 22854 metustexhalf 22859 restmetu 22873 rrxcph 23688 rrxsuppss 23699 mdegfval 24349 mdegleb 24351 mdegldg 24353 deg1mul3le 24403 plyeq0lem 24493 dgrcl 24516 dgrub 24517 dgrlb 24519 vieta1lem1 24592 suppovss 30176 dimkerim 30608 fedgmullem1 30610 carsggect 31178 sibfof 31200 eulerpartlemsv2 31218 eulerpartlemsf 31219 eulerpartlemt 31231 eulerpartlemgu 31237 eulerpartlemgs2 31240 cvmliftmolem1 32073 cvmlift3lem6 32116 itg2addnclem 34332 keridl 34700 ismrcd1 38635 istopclsd 38637 pwfi2f1o 39037 sge0f1o 42041 smfsuplem1 42462 |
Copyright terms: Public domain | W3C validator |