Theorem fssdm 6710

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

Syntax hints:   → wi 4   ⊆ wss 3917  dom cdm 5641  ⟶wf 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934  df-fn 6517  df-f 6518

This theorem is referenced by:  fisuppfi  9329  wemapso  9511  wemapso2lem  9512  cantnfcl  9627  cantnfle  9631  cantnflt  9632  cantnff  9634  cantnfp1lem3  9640  cantnflem1b  9646  cantnflem1  9649  cantnflem3  9651  cnfcomlem  9659  cnfcom  9660  cnfcom3lem  9663  cnfcom3  9664  fin1a2lem7  10366  isercolllem2  15639  isercolllem3  15640  fsumss  15698  fprodss  15921  vdwlem1  16959  vdwlem5  16963  vdwlem6  16964  ghmpreima  19177  pmtrfconj  19403  gsumval3lem1  19842  gsumval3lem2  19843  gsumval3  19844  gsumzres  19846  gsumzcl2  19847  gsumzf1o  19849  gsumzmhm  19874  gsumzoppg  19881  gsum2d  19909  dpjidcl  19997  lmhmpreima  20962  rhmpreimaidl  21194  gsumfsum  21358  regsumsupp  21538  frlmlbs  21713  mplcoe1  21951  mplcoe5  21954  psr1baslem  22076  mdetdiaglem  22492  cnclima  23162  iscncl  23163  cnclsi  23166  txcnmpt  23518  qtopval2  23590  qtopcn  23608  rnelfmlem  23846  fmfnfmlem4  23851  clssubg  24003  tgphaus  24011  tsmsgsum  24033  xmeter  24328  metustss  24446  metustexhalf  24451  restmetu  24465  rrxcph  25299  rrxsuppss  25310  mdegfval  25974  mdegleb  25976  mdegldg  25978  deg1mul3le  26029  plyeq0lem  26122  dgrcl  26145  dgrub  26146  dgrlb  26148  vieta1lem1  26225  suppovss  32611  pwrssmgc  32933  gsumfs2d  33002  gsumhashmul  33008  elrgspnlem4  33203  elrgspnsubrunlem1  33205  elrspunidl  33406  rprmdvdsprod  33512  1arithidom  33515  dimkerim  33630  fedgmullem1  33632  lvecendof1f1o  33636  fldextrspunlsplem  33675  carsggect  34316  sibfof  34338  eulerpartlemsv2  34356  eulerpartlemsf  34357  eulerpartlemt  34369  eulerpartlemgu  34375  eulerpartlemgs2  34378  cvmliftmolem1  35275  cvmlift3lem6  35318  itg2addnclem  37672  keridl  38033  ismrcd1  42693  istopclsd  42695  pwfi2f1o  43092  sge0f1o  46387  smfsuplem1  46816