Theorem fssdm 6678

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

Syntax hints:   → wi 4   ⊆ wss 3898  dom cdm 5621  ⟶wf 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3915  df-fn 6492  df-f 6493

This theorem is referenced by:  fisuppfi  9266  wemapso  9448  wemapso2lem  9449  cantnfcl  9568  cantnfle  9572  cantnflt  9573  cantnff  9575  cantnfp1lem3  9581  cantnflem1b  9587  cantnflem1  9590  cantnflem3  9592  cnfcomlem  9600  cnfcom  9601  cnfcom3lem  9604  cnfcom3  9605  fin1a2lem7  10308  isercolllem2  15580  isercolllem3  15581  fsumss  15639  fprodss  15862  vdwlem1  16900  vdwlem5  16904  vdwlem6  16905  ghmpreima  19158  pmtrfconj  19386  gsumval3lem1  19825  gsumval3lem2  19826  gsumval3  19827  gsumzres  19829  gsumzcl2  19830  gsumzf1o  19832  gsumzmhm  19857  gsumzoppg  19864  gsum2d  19892  dpjidcl  19980  lmhmpreima  20991  rhmpreimaidl  21223  gsumfsum  21380  regsumsupp  21568  frlmlbs  21743  mplcoe1  21983  mplcoe5  21986  psr1baslem  22116  mdetdiaglem  22533  cnclima  23203  iscncl  23204  cnclsi  23207  txcnmpt  23559  qtopval2  23631  qtopcn  23649  rnelfmlem  23887  fmfnfmlem4  23892  clssubg  24044  tgphaus  24052  tsmsgsum  24074  xmeter  24368  metustss  24486  metustexhalf  24491  restmetu  24505  rrxcph  25339  rrxsuppss  25350  mdegfval  26014  mdegleb  26016  mdegldg  26018  deg1mul3le  26069  plyeq0lem  26162  dgrcl  26185  dgrub  26186  dgrlb  26188  vieta1lem1  26265  suppovss  32686  pwrssmgc  33010  gsumfs2d  33072  gsumhashmul  33078  elrgspnlem4  33255  elrgspnsubrunlem1  33257  elrspunidl  33437  rprmdvdsprod  33543  1arithidom  33546  esplyfv1  33655  esplysply  33657  esplyfval3  33658  dimkerim  33712  fedgmullem1  33714  lvecendof1f1o  33718  fldextrspunlsplem  33758  carsggect  34403  sibfof  34425  eulerpartlemsv2  34443  eulerpartlemsf  34444  eulerpartlemt  34456  eulerpartlemgu  34462  eulerpartlemgs2  34465  cvmliftmolem1  35397  cvmlift3lem6  35440  itg2addnclem  37784  keridl  38145  ismrcd1  42855  istopclsd  42857  pwfi2f1o  43253  sge0f1o  46542  smfsuplem1  46971