Theorem fssdm 6504

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

Syntax hints:   → wi 4   ⊆ wss 3881  dom cdm 5519  ⟶wf 6320

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-fn 6327  df-f 6328

This theorem is referenced by:  fisuppfi  8825  wemapso  8999  wemapso2lem  9000  cantnfcl  9114  cantnfle  9118  cantnflt  9119  cantnff  9121  cantnfp1lem3  9127  cantnflem1b  9133  cantnflem1  9136  cantnflem3  9138  cnfcomlem  9146  cnfcom  9147  cnfcom3lem  9150  cnfcom3  9151  fin1a2lem7  9817  isercolllem2  15014  isercolllem3  15015  fsumss  15074  fprodss  15294  vdwlem1  16307  vdwlem5  16311  vdwlem6  16312  ghmpreima  18372  pmtrfconj  18586  gsumval3lem1  19018  gsumval3lem2  19019  gsumval3  19020  gsumzres  19022  gsumzcl2  19023  gsumzf1o  19025  gsumzmhm  19050  gsumzoppg  19057  gsum2d  19085  dpjidcl  19173  lmhmpreima  19813  gsumfsum  20158  regsumsupp  20311  frlmlbs  20486  mplcoe1  20705  mplcoe5  20708  psr1baslem  20814  mdetdiaglem  21203  cnclima  21873  iscncl  21874  cnclsi  21877  txcnmpt  22229  qtopval2  22301  qtopcn  22319  rnelfmlem  22557  fmfnfmlem4  22562  clssubg  22714  tgphaus  22722  tsmsgsum  22744  xmeter  23040  metustss  23158  metustexhalf  23163  restmetu  23177  rrxcph  23996  rrxsuppss  24007  mdegfval  24663  mdegleb  24665  mdegldg  24667  deg1mul3le  24717  plyeq0lem  24807  dgrcl  24830  dgrub  24831  dgrlb  24833  vieta1lem1  24906  suppovss  30443  pwrssmgc  30706  gsumhashmul  30741  rhmpreimaidl  31011  elrspunidl  31014  dimkerim  31111  fedgmullem1  31113  carsggect  31686  sibfof  31708  eulerpartlemsv2  31726  eulerpartlemsf  31727  eulerpartlemt  31739  eulerpartlemgu  31745  eulerpartlemgs2  31748  cvmliftmolem1  32641  cvmlift3lem6  32684  itg2addnclem  35108  keridl  35470  ismrcd1  39639  istopclsd  39641  pwfi2f1o  40040  sge0f1o  43021  smfsuplem1  43442