Theorem fssdm 6722

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3899  dom cdm 5655  ⟶wf 6529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ss 3916  df-fn 6536  df-f 6537

This theorem is used by:  fisuppfi  9341  wemapso  9523  wemapso2lem  9524  cantnfcl  9646  cantnfle  9650  cantnflt  9651  cantnff  9653  cantnfp1lem3  9659  cantnflem1b  9665  cantnflem1  9668  cantnflem3  9670  cnfcomlem  9678  cnfcom  9679  cnfcom3lem  9682  cnfcom3  9683  fin1a2lem7  10408  isercolllem2  15753  isercolllem3  15754  fsumss  15811  fprodss  16035  vdwlem1  17073  vdwlem5  17077  vdwlem6  17078  ghmpreima  19365  pmtrfconj  19593  gsumval3lem1  20032  gsumval3lem2  20033  gsumval3  20034  gsumzres  20036  gsumzcl2  20037  gsumzf1o  20039  gsumzmhm  20064  gsumzoppg  20071  gsum2d  20099  dpjidcl  20187  lmhmpreima  21232  rhmpreimaidl  21479  gsumfsum  21647  regsumsupp  21835  frlmlbs  22010  mplcoe1  22253  mplcoe5  22256  psr1baslem  22410  mdetdiaglem  22820  cnclima  23493  iscncl  23494  cnclsi  23497  txcnmpt  23850  qtopval2  23922  qtopcn  23940  rnelfmlem  24178  fmfnfmlem4  24183  clssubg  24335  tgphaus  24343  tsmsgsum  24365  xmeter  24659  metustss  24777  metustexhalf  24782  restmetu  24796  rrxcph  25620  rrxsuppss  25631  mdegfval  26287  mdegleb  26289  mdegldg  26291  deg1mul3le  26342  plyeq0lem  26436  dgrcl  26459  dgrub  26460  dgrlb  26462  vieta1lem1  26542  suppovss  33153  pwrssmgc  33440  gsumfs2d  33501  gsumhashmul  33507  elrgspnlem4  33685  elrgspnsubrunlem1  33687  elrspunidl  33856  rprmdvdsprod  33944  1arithidom  33947  esplyfv1  34079  esplysply  34081  esplyfval3  34082  esplyfvaln  34084  dimkerim  34137  fedgmullem1  34139  lvecendof1f1o  34143  fldextrspunlsplem  34183  carsggect  34829  sibfof  34851  eulerpartlemsv2  34869  eulerpartlemsf  34870  eulerpartlemt  34882  eulerpartlemgu  34888  eulerpartlemgs2  34891  cvmliftmolem1  35860  cvmlift3lem6  35903  itg2addnclem  38420  keridl  38782  ismrcd1  43543  istopclsd  43545  pwfi2f1o  43937  sge0f1o  47210  smfsuplem1  47639