Theorem fssdm 6734

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

Syntax hints:   → wi 4   ⊆ wss 3947  dom cdm 5675  ⟶wf 6536

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-fn 6543  df-f 6544

This theorem is referenced by:  fisuppfi  9366  wemapso  9542  wemapso2lem  9543  cantnfcl  9658  cantnfle  9662  cantnflt  9663  cantnff  9665  cantnfp1lem3  9671  cantnflem1b  9677  cantnflem1  9680  cantnflem3  9682  cnfcomlem  9690  cnfcom  9691  cnfcom3lem  9694  cnfcom3  9695  fin1a2lem7  10397  isercolllem2  15608  isercolllem3  15609  fsumss  15667  fprodss  15888  vdwlem1  16910  vdwlem5  16914  vdwlem6  16915  ghmpreima  19108  pmtrfconj  19328  gsumval3lem1  19767  gsumval3lem2  19768  gsumval3  19769  gsumzres  19771  gsumzcl2  19772  gsumzf1o  19774  gsumzmhm  19799  gsumzoppg  19806  gsum2d  19834  dpjidcl  19922  lmhmpreima  20651  gsumfsum  21004  regsumsupp  21166  frlmlbs  21343  mplcoe1  21583  mplcoe5  21586  psr1baslem  21700  mdetdiaglem  22091  cnclima  22763  iscncl  22764  cnclsi  22767  txcnmpt  23119  qtopval2  23191  qtopcn  23209  rnelfmlem  23447  fmfnfmlem4  23452  clssubg  23604  tgphaus  23612  tsmsgsum  23634  xmeter  23930  metustss  24051  metustexhalf  24056  restmetu  24070  rrxcph  24900  rrxsuppss  24911  mdegfval  25571  mdegleb  25573  mdegldg  25575  deg1mul3le  25625  plyeq0lem  25715  dgrcl  25738  dgrub  25739  dgrlb  25741  vieta1lem1  25814  suppovss  31893  pwrssmgc  32157  gsumhashmul  32195  rhmpreimaidl  32525  elrspunidl  32534  dimkerim  32700  fedgmullem1  32702  carsggect  33305  sibfof  33327  eulerpartlemsv2  33345  eulerpartlemsf  33346  eulerpartlemt  33358  eulerpartlemgu  33364  eulerpartlemgs2  33367  cvmliftmolem1  34260  cvmlift3lem6  34303  itg2addnclem  36527  keridl  36888  ismrcd1  41421  istopclsd  41423  pwfi2f1o  41823  sge0f1o  45084  smfsuplem1  45513