Theorem fssdm 6687

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

Syntax hints:   → wi 4   ⊆ wss 3889  dom cdm 5631  ⟶wf 6494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906  df-fn 6501  df-f 6502

This theorem is referenced by:  fisuppfi  9284  wemapso  9466  wemapso2lem  9467  cantnfcl  9588  cantnfle  9592  cantnflt  9593  cantnff  9595  cantnfp1lem3  9601  cantnflem1b  9607  cantnflem1  9610  cantnflem3  9612  cnfcomlem  9620  cnfcom  9621  cnfcom3lem  9624  cnfcom3  9625  fin1a2lem7  10328  isercolllem2  15628  isercolllem3  15629  fsumss  15687  fprodss  15913  vdwlem1  16952  vdwlem5  16956  vdwlem6  16957  ghmpreima  19213  pmtrfconj  19441  gsumval3lem1  19880  gsumval3lem2  19881  gsumval3  19882  gsumzres  19884  gsumzcl2  19885  gsumzf1o  19887  gsumzmhm  19912  gsumzoppg  19919  gsum2d  19947  dpjidcl  20035  lmhmpreima  21043  rhmpreimaidl  21275  gsumfsum  21414  regsumsupp  21602  frlmlbs  21777  mplcoe1  22015  mplcoe5  22018  psr1baslem  22148  mdetdiaglem  22563  cnclima  23233  iscncl  23234  cnclsi  23237  txcnmpt  23589  qtopval2  23661  qtopcn  23679  rnelfmlem  23917  fmfnfmlem4  23922  clssubg  24074  tgphaus  24082  tsmsgsum  24104  xmeter  24398  metustss  24516  metustexhalf  24521  restmetu  24535  rrxcph  25359  rrxsuppss  25370  mdegfval  26027  mdegleb  26029  mdegldg  26031  deg1mul3le  26082  plyeq0lem  26175  dgrcl  26198  dgrub  26199  dgrlb  26201  vieta1lem1  26276  suppovss  32754  pwrssmgc  33060  gsumfs2d  33122  gsumhashmul  33128  elrgspnlem4  33306  elrgspnsubrunlem1  33308  elrspunidl  33488  rprmdvdsprod  33594  1arithidom  33597  esplyfv1  33713  esplysply  33715  esplyfval3  33716  esplyfvaln  33718  dimkerim  33771  fedgmullem1  33773  lvecendof1f1o  33777  fldextrspunlsplem  33817  carsggect  34462  sibfof  34484  eulerpartlemsv2  34502  eulerpartlemsf  34503  eulerpartlemt  34515  eulerpartlemgu  34521  eulerpartlemgs2  34524  cvmliftmolem1  35463  cvmlift3lem6  35506  itg2addnclem  37992  keridl  38353  ismrcd1  43130  istopclsd  43132  pwfi2f1o  43524  sge0f1o  46810  smfsuplem1  47239