Theorem fssdm 6679

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

Syntax hints:   → wi 4   ⊆ wss 3890  dom cdm 5622  ⟶wf 6486

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907  df-fn 6493  df-f 6494

This theorem is referenced by:  fisuppfi  9275  wemapso  9457  wemapso2lem  9458  cantnfcl  9577  cantnfle  9581  cantnflt  9582  cantnff  9584  cantnfp1lem3  9590  cantnflem1b  9596  cantnflem1  9599  cantnflem3  9601  cnfcomlem  9609  cnfcom  9610  cnfcom3lem  9613  cnfcom3  9614  fin1a2lem7  10317  isercolllem2  15590  isercolllem3  15591  fsumss  15649  fprodss  15872  vdwlem1  16910  vdwlem5  16914  vdwlem6  16915  ghmpreima  19171  pmtrfconj  19399  gsumval3lem1  19838  gsumval3lem2  19839  gsumval3  19840  gsumzres  19842  gsumzcl2  19843  gsumzf1o  19845  gsumzmhm  19870  gsumzoppg  19877  gsum2d  19905  dpjidcl  19993  lmhmpreima  21002  rhmpreimaidl  21234  gsumfsum  21391  regsumsupp  21579  frlmlbs  21754  mplcoe1  21993  mplcoe5  21996  psr1baslem  22126  mdetdiaglem  22541  cnclima  23211  iscncl  23212  cnclsi  23215  txcnmpt  23567  qtopval2  23639  qtopcn  23657  rnelfmlem  23895  fmfnfmlem4  23900  clssubg  24052  tgphaus  24060  tsmsgsum  24082  xmeter  24376  metustss  24494  metustexhalf  24499  restmetu  24513  rrxcph  25337  rrxsuppss  25348  mdegfval  26008  mdegleb  26010  mdegldg  26012  deg1mul3le  26063  plyeq0lem  26156  dgrcl  26179  dgrub  26180  dgrlb  26182  vieta1lem1  26258  suppovss  32743  pwrssmgc  33065  gsumfs2d  33127  gsumhashmul  33133  elrgspnlem4  33311  elrgspnsubrunlem1  33313  elrspunidl  33493  rprmdvdsprod  33599  1arithidom  33602  esplyfv1  33718  esplysply  33720  esplyfval3  33721  esplyfvaln  33723  dimkerim  33777  fedgmullem1  33779  lvecendof1f1o  33783  fldextrspunlsplem  33823  carsggect  34468  sibfof  34490  eulerpartlemsv2  34508  eulerpartlemsf  34509  eulerpartlemt  34521  eulerpartlemgu  34527  eulerpartlemgs2  34530  cvmliftmolem1  35469  cvmlift3lem6  35512  itg2addnclem  37983  keridl  38344  ismrcd1  43129  istopclsd  43131  pwfi2f1o  43527  sge0f1o  46814  smfsuplem1  47243