Theorem fssdm 6665

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 6656	. 2 ⊢ (𝜑 → dom 𝐹 = 𝐴)
4	1, 3	sseqtrid 3972	1 ⊢ (𝜑 → 𝐷 ⊆ 𝐴)

Syntax hints:   → wi 4   ⊆ wss 3897  dom cdm 5611  ⟶wf 6472

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 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3914  df-fn 6479  df-f 6480

This theorem is referenced by:  fisuppfi  9250  wemapso  9432  wemapso2lem  9433  cantnfcl  9552  cantnfle  9556  cantnflt  9557  cantnff  9559  cantnfp1lem3  9565  cantnflem1b  9571  cantnflem1  9574  cantnflem3  9576  cnfcomlem  9584  cnfcom  9585  cnfcom3lem  9588  cnfcom3  9589  fin1a2lem7  10292  isercolllem2  15568  isercolllem3  15569  fsumss  15627  fprodss  15850  vdwlem1  16888  vdwlem5  16892  vdwlem6  16893  ghmpreima  19145  pmtrfconj  19373  gsumval3lem1  19812  gsumval3lem2  19813  gsumval3  19814  gsumzres  19816  gsumzcl2  19817  gsumzf1o  19819  gsumzmhm  19844  gsumzoppg  19851  gsum2d  19879  dpjidcl  19967  lmhmpreima  20977  rhmpreimaidl  21209  gsumfsum  21366  regsumsupp  21554  frlmlbs  21729  mplcoe1  21967  mplcoe5  21970  psr1baslem  22092  mdetdiaglem  22508  cnclima  23178  iscncl  23179  cnclsi  23182  txcnmpt  23534  qtopval2  23606  qtopcn  23624  rnelfmlem  23862  fmfnfmlem4  23867  clssubg  24019  tgphaus  24027  tsmsgsum  24049  xmeter  24343  metustss  24461  metustexhalf  24466  restmetu  24480  rrxcph  25314  rrxsuppss  25325  mdegfval  25989  mdegleb  25991  mdegldg  25993  deg1mul3le  26044  plyeq0lem  26137  dgrcl  26160  dgrub  26161  dgrlb  26163  vieta1lem1  26240  suppovss  32654  pwrssmgc  32973  gsumfs2d  33027  gsumhashmul  33033  elrgspnlem4  33204  elrgspnsubrunlem1  33206  elrspunidl  33385  rprmdvdsprod  33491  1arithidom  33494  esplyfv1  33582  esplysply  33584  dimkerim  33632  fedgmullem1  33634  lvecendof1f1o  33638  fldextrspunlsplem  33678  carsggect  34323  sibfof  34345  eulerpartlemsv2  34363  eulerpartlemsf  34364  eulerpartlemt  34376  eulerpartlemgu  34382  eulerpartlemgs2  34385  cvmliftmolem1  35317  cvmlift3lem6  35360  itg2addnclem  37711  keridl  38072  ismrcd1  42731  istopclsd  42733  pwfi2f1o  43129  sge0f1o  46420  smfsuplem1  46849