Theorem fssdm 6530

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.)

Hypotheses

Ref	Expression
fssdm.d	⊢ 𝐷 ⊆ dom 𝐹
fssdm.f	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)

Assertion

Ref	Expression
fssdm	⊢ (𝜑 → 𝐷 ⊆ 𝐴)

Proof of Theorem 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 ⊢ (𝜑 → 𝐷 ⊆ 𝐴)

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