Theorem fssdm 6675

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

Syntax hints:   → wi 4   ⊆ wss 3905  dom cdm 5623  ⟶wf 6482

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 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3922  df-fn 6489  df-f 6490

This theorem is referenced by:  fisuppfi  9280  wemapso  9462  wemapso2lem  9463  cantnfcl  9582  cantnfle  9586  cantnflt  9587  cantnff  9589  cantnfp1lem3  9595  cantnflem1b  9601  cantnflem1  9604  cantnflem3  9606  cnfcomlem  9614  cnfcom  9615  cnfcom3lem  9618  cnfcom3  9619  fin1a2lem7  10319  isercolllem2  15591  isercolllem3  15592  fsumss  15650  fprodss  15873  vdwlem1  16911  vdwlem5  16915  vdwlem6  16916  ghmpreima  19135  pmtrfconj  19363  gsumval3lem1  19802  gsumval3lem2  19803  gsumval3  19804  gsumzres  19806  gsumzcl2  19807  gsumzf1o  19809  gsumzmhm  19834  gsumzoppg  19841  gsum2d  19869  dpjidcl  19957  lmhmpreima  20970  rhmpreimaidl  21202  gsumfsum  21359  regsumsupp  21547  frlmlbs  21722  mplcoe1  21960  mplcoe5  21963  psr1baslem  22085  mdetdiaglem  22501  cnclima  23171  iscncl  23172  cnclsi  23175  txcnmpt  23527  qtopval2  23599  qtopcn  23617  rnelfmlem  23855  fmfnfmlem4  23860  clssubg  24012  tgphaus  24020  tsmsgsum  24042  xmeter  24337  metustss  24455  metustexhalf  24460  restmetu  24474  rrxcph  25308  rrxsuppss  25319  mdegfval  25983  mdegleb  25985  mdegldg  25987  deg1mul3le  26038  plyeq0lem  26131  dgrcl  26154  dgrub  26155  dgrlb  26157  vieta1lem1  26234  suppovss  32637  pwrssmgc  32955  gsumfs2d  33021  gsumhashmul  33027  elrgspnlem4  33198  elrgspnsubrunlem1  33200  elrspunidl  33378  rprmdvdsprod  33484  1arithidom  33487  dimkerim  33602  fedgmullem1  33604  lvecendof1f1o  33608  fldextrspunlsplem  33647  carsggect  34288  sibfof  34310  eulerpartlemsv2  34328  eulerpartlemsf  34329  eulerpartlemt  34341  eulerpartlemgu  34347  eulerpartlemgs2  34350  cvmliftmolem1  35256  cvmlift3lem6  35299  itg2addnclem  37653  keridl  38014  ismrcd1  42674  istopclsd  42676  pwfi2f1o  43072  sge0f1o  46367  smfsuplem1  46796