Theorem fssdm 6766

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

Syntax hints:   → wi 4   ⊆ wss 3976  dom cdm 5700  ⟶wf 6569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993  df-fn 6576  df-f 6577

This theorem is referenced by:  fisuppfi  9441  wemapso  9620  wemapso2lem  9621  cantnfcl  9736  cantnfle  9740  cantnflt  9741  cantnff  9743  cantnfp1lem3  9749  cantnflem1b  9755  cantnflem1  9758  cantnflem3  9760  cnfcomlem  9768  cnfcom  9769  cnfcom3lem  9772  cnfcom3  9773  fin1a2lem7  10475  isercolllem2  15714  isercolllem3  15715  fsumss  15773  fprodss  15996  vdwlem1  17028  vdwlem5  17032  vdwlem6  17033  ghmpreima  19278  pmtrfconj  19508  gsumval3lem1  19947  gsumval3lem2  19948  gsumval3  19949  gsumzres  19951  gsumzcl2  19952  gsumzf1o  19954  gsumzmhm  19979  gsumzoppg  19986  gsum2d  20014  dpjidcl  20102  lmhmpreima  21070  rhmpreimaidl  21310  gsumfsum  21475  regsumsupp  21663  frlmlbs  21840  mplcoe1  22078  mplcoe5  22081  psr1baslem  22207  mdetdiaglem  22625  cnclima  23297  iscncl  23298  cnclsi  23301  txcnmpt  23653  qtopval2  23725  qtopcn  23743  rnelfmlem  23981  fmfnfmlem4  23986  clssubg  24138  tgphaus  24146  tsmsgsum  24168  xmeter  24464  metustss  24585  metustexhalf  24590  restmetu  24604  rrxcph  25445  rrxsuppss  25456  mdegfval  26121  mdegleb  26123  mdegldg  26125  deg1mul3le  26176  plyeq0lem  26269  dgrcl  26292  dgrub  26293  dgrlb  26295  vieta1lem1  26370  suppovss  32697  pwrssmgc  32973  gsumhashmul  33040  elrspunidl  33421  rprmdvdsprod  33527  1arithidom  33530  dimkerim  33640  fedgmullem1  33642  lvecendof1f1o  33646  carsggect  34283  sibfof  34305  eulerpartlemsv2  34323  eulerpartlemsf  34324  eulerpartlemt  34336  eulerpartlemgu  34342  eulerpartlemgs2  34345  cvmliftmolem1  35249  cvmlift3lem6  35292  itg2addnclem  37631  keridl  37992  ismrcd1  42654  istopclsd  42656  pwfi2f1o  43053  sge0f1o  46303  smfsuplem1  46732