Theorem fssdm 6727

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916  df-fn 6540  df-f 6541

This theorem is used by:  fisuppfi  9356  wemapso  9538  wemapso2lem  9539  cantnfcl  9661  cantnfle  9665  cantnflt  9666  cantnff  9668  cantnfp1lem3  9674  cantnflem1b  9680  cantnflem1  9683  cantnflem3  9685  cnfcomlem  9693  cnfcom  9694  cnfcom3lem  9697  cnfcom3  9698  fin1a2lem7  10477  isercolllem2  15826  isercolllem3  15827  fsumss  15884  fprodss  16108  vdwlem1  17152  vdwlem5  17156  vdwlem6  17157  ghmpreima  19445  pmtrfconj  19673  gsumval3lem1  20112  gsumval3lem2  20113  gsumval3  20114  gsumzres  20116  gsumzcl2  20117  gsumzf1o  20119  gsumzmhm  20144  gsumzoppg  20151  gsum2d  20179  dpjidcl  20267  lmhmpreima  21316  rhmpreimaidl  21564  gsumfsum  21733  regsumsupp  21921  frlmlbs  22096  mplcoe1  22339  mplcoe5  22342  psr1baslem  22496  mdetdiaglem  22906  cnclima  23579  iscncl  23580  cnclsi  23583  txcnmpt  23936  qtopval2  24008  qtopcn  24026  rnelfmlem  24264  fmfnfmlem4  24269  clssubg  24421  tgphaus  24429  tsmsgsum  24451  xmeter  24745  metustss  24863  metustexhalf  24868  restmetu  24882  rrxcph  25706  rrxsuppss  25717  mdegfval  26373  mdegleb  26375  mdegldg  26377  deg1mul3le  26428  plyeq0lem  26522  dgrcl  26545  dgrub  26546  dgrlb  26548  vieta1lem1  26626  suppovss  33267  pwrssmgc  33554  gsumfs2d  33615  gsumhashmul  33621  elrgspnlem4  33799  elrgspnsubrunlem1  33801  elrspunidl  33971  rprmdvdsprod  34059  1arithidom  34062  esplyfv1  34194  esplysply  34196  esplyfval3  34197  esplyfvaln  34199  dimkerim  34252  fedgmullem1  34254  lvecendof1f1o  34258  fldextrspunlsplem  34298  carsggect  34943  sibfof  34965  eulerpartlemsv2  34983  eulerpartlemsf  34984  eulerpartlemt  34996  eulerpartlemgu  35002  eulerpartlemgs2  35005  cvmliftmolem1  36025  cvmlift3lem6  36068  itg2addnclem  38569  keridl  38946  ismrcd1  43688  istopclsd  43690  pwfi2f1o  44082  sge0f1o  47361  smfsuplem1  47790