Theorem fssdm 6725

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

Syntax hints:   → wi 4   ⊆ wss 3926  dom cdm 5654  ⟶wf 6527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ss 3943  df-fn 6534  df-f 6535

This theorem is referenced by:  fisuppfi  9383  wemapso  9565  wemapso2lem  9566  cantnfcl  9681  cantnfle  9685  cantnflt  9686  cantnff  9688  cantnfp1lem3  9694  cantnflem1b  9700  cantnflem1  9703  cantnflem3  9705  cnfcomlem  9713  cnfcom  9714  cnfcom3lem  9717  cnfcom3  9718  fin1a2lem7  10420  isercolllem2  15682  isercolllem3  15683  fsumss  15741  fprodss  15964  vdwlem1  17001  vdwlem5  17005  vdwlem6  17006  ghmpreima  19221  pmtrfconj  19447  gsumval3lem1  19886  gsumval3lem2  19887  gsumval3  19888  gsumzres  19890  gsumzcl2  19891  gsumzf1o  19893  gsumzmhm  19918  gsumzoppg  19925  gsum2d  19953  dpjidcl  20041  lmhmpreima  21006  rhmpreimaidl  21238  gsumfsum  21402  regsumsupp  21582  frlmlbs  21757  mplcoe1  21995  mplcoe5  21998  psr1baslem  22120  mdetdiaglem  22536  cnclima  23206  iscncl  23207  cnclsi  23210  txcnmpt  23562  qtopval2  23634  qtopcn  23652  rnelfmlem  23890  fmfnfmlem4  23895  clssubg  24047  tgphaus  24055  tsmsgsum  24077  xmeter  24372  metustss  24490  metustexhalf  24495  restmetu  24509  rrxcph  25344  rrxsuppss  25355  mdegfval  26019  mdegleb  26021  mdegldg  26023  deg1mul3le  26074  plyeq0lem  26167  dgrcl  26190  dgrub  26191  dgrlb  26193  vieta1lem1  26270  suppovss  32658  pwrssmgc  32980  gsumfs2d  33049  gsumhashmul  33055  elrgspnlem4  33240  elrgspnsubrunlem1  33242  elrspunidl  33443  rprmdvdsprod  33549  1arithidom  33552  dimkerim  33667  fedgmullem1  33669  lvecendof1f1o  33673  fldextrspunlsplem  33714  carsggect  34350  sibfof  34372  eulerpartlemsv2  34390  eulerpartlemsf  34391  eulerpartlemt  34403  eulerpartlemgu  34409  eulerpartlemgs2  34412  cvmliftmolem1  35303  cvmlift3lem6  35346  itg2addnclem  37695  keridl  38056  ismrcd1  42721  istopclsd  42723  pwfi2f1o  43120  sge0f1o  46411  smfsuplem1  46840