Theorem fssdm 6604

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

Syntax hints:   → wi 4   ⊆ wss 3883  dom cdm 5580  ⟶wf 6414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-fn 6421  df-f 6422

This theorem is referenced by:  fisuppfi  9066  wemapso  9240  wemapso2lem  9241  cantnfcl  9355  cantnfle  9359  cantnflt  9360  cantnff  9362  cantnfp1lem3  9368  cantnflem1b  9374  cantnflem1  9377  cantnflem3  9379  cnfcomlem  9387  cnfcom  9388  cnfcom3lem  9391  cnfcom3  9392  fin1a2lem7  10093  isercolllem2  15305  isercolllem3  15306  fsumss  15365  fprodss  15586  vdwlem1  16610  vdwlem5  16614  vdwlem6  16615  ghmpreima  18771  pmtrfconj  18989  gsumval3lem1  19421  gsumval3lem2  19422  gsumval3  19423  gsumzres  19425  gsumzcl2  19426  gsumzf1o  19428  gsumzmhm  19453  gsumzoppg  19460  gsum2d  19488  dpjidcl  19576  lmhmpreima  20225  gsumfsum  20577  regsumsupp  20739  frlmlbs  20914  mplcoe1  21148  mplcoe5  21151  psr1baslem  21266  mdetdiaglem  21655  cnclima  22327  iscncl  22328  cnclsi  22331  txcnmpt  22683  qtopval2  22755  qtopcn  22773  rnelfmlem  23011  fmfnfmlem4  23016  clssubg  23168  tgphaus  23176  tsmsgsum  23198  xmeter  23494  metustss  23613  metustexhalf  23618  restmetu  23632  rrxcph  24461  rrxsuppss  24472  mdegfval  25132  mdegleb  25134  mdegldg  25136  deg1mul3le  25186  plyeq0lem  25276  dgrcl  25299  dgrub  25300  dgrlb  25302  vieta1lem1  25375  suppovss  30919  pwrssmgc  31180  gsumhashmul  31218  rhmpreimaidl  31505  elrspunidl  31508  dimkerim  31610  fedgmullem1  31612  carsggect  32185  sibfof  32207  eulerpartlemsv2  32225  eulerpartlemsf  32226  eulerpartlemt  32238  eulerpartlemgu  32244  eulerpartlemgs2  32247  cvmliftmolem1  33143  cvmlift3lem6  33186  itg2addnclem  35755  keridl  36117  ismrcd1  40436  istopclsd  40438  pwfi2f1o  40837  sge0f1o  43810  smfsuplem1  44231