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 6523 | . 2 ⊢ (𝜑 → dom 𝐹 = 𝐴) |
4 | 1, 3 | sseqtrid 4019 | 1 ⊢ (𝜑 → 𝐷 ⊆ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3936 dom cdm 5555 ⟶wf 6351 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-in 3943 df-ss 3952 df-fn 6358 df-f 6359 |
This theorem is referenced by: fisuppfi 8841 wemapso 9015 wemapso2lem 9016 cantnfcl 9130 cantnfle 9134 cantnflt 9135 cantnff 9137 cantnfp1lem3 9143 cantnflem1b 9149 cantnflem1 9152 cantnflem3 9154 cnfcomlem 9162 cnfcom 9163 cnfcom3lem 9166 cnfcom3 9167 fin1a2lem7 9828 isercolllem2 15022 isercolllem3 15023 fsumss 15082 fprodss 15302 vdwlem1 16317 vdwlem5 16321 vdwlem6 16322 ghmpreima 18380 pmtrfconj 18594 gsumval3lem1 19025 gsumval3lem2 19026 gsumval3 19027 gsumzres 19029 gsumzcl2 19030 gsumzf1o 19032 gsumzmhm 19057 gsumzoppg 19064 gsum2d 19092 dpjidcl 19180 lmhmpreima 19820 mplcoe1 20246 mplcoe5 20249 psr1baslem 20353 gsumfsum 20612 regsumsupp 20766 frlmlbs 20941 mdetdiaglem 21207 cnclima 21876 iscncl 21877 cnclsi 21880 txcnmpt 22232 qtopval2 22304 qtopcn 22322 rnelfmlem 22560 fmfnfmlem4 22565 clssubg 22717 tgphaus 22725 tsmsgsum 22747 xmeter 23043 metustss 23161 metustexhalf 23166 restmetu 23180 rrxcph 23995 rrxsuppss 24006 mdegfval 24656 mdegleb 24658 mdegldg 24660 deg1mul3le 24710 plyeq0lem 24800 dgrcl 24823 dgrub 24824 dgrlb 24826 vieta1lem1 24899 suppovss 30426 dimkerim 31023 fedgmullem1 31025 carsggect 31576 sibfof 31598 eulerpartlemsv2 31616 eulerpartlemsf 31617 eulerpartlemt 31629 eulerpartlemgu 31635 eulerpartlemgs2 31638 cvmliftmolem1 32528 cvmlift3lem6 32571 itg2addnclem 34958 keridl 35325 ismrcd1 39315 istopclsd 39317 pwfi2f1o 39716 sge0f1o 42684 smfsuplem1 43105 |
Copyright terms: Public domain | W3C validator |