Theorem fssdm 6727

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

Syntax hints:   → wi 4   ⊆ wss 3906  dom cdm 5663  ⟶wf 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923  df-fn 6541  df-f 6542

This theorem is referenced by:  fisuppfi  9332  wemapso  9514  wemapso2lem  9515  cantnfcl  9637  cantnfle  9641  cantnflt  9642  cantnff  9644  cantnfp1lem3  9650  cantnflem1b  9656  cantnflem1  9659  cantnflem3  9661  cnfcomlem  9669  cnfcom  9670  cnfcom3lem  9673  cnfcom3  9674  fin1a2lem7  10391  isercolllem2  15719  isercolllem3  15720  fsumss  15778  fprodss  16004  vdwlem1  17042  vdwlem5  17046  vdwlem6  17047  ghmpreima  19309  pmtrfconj  19537  gsumval3lem1  19976  gsumval3lem2  19977  gsumval3  19978  gsumzres  19980  gsumzcl2  19981  gsumzf1o  19983  gsumzmhm  20008  gsumzoppg  20015  gsum2d  20043  dpjidcl  20131  lmhmpreima  21150  rhmpreimaidl  21397  gsumfsum  21565  regsumsupp  21753  frlmlbs  21928  mplcoe1  22169  mplcoe5  22172  psr1baslem  22326  mdetdiaglem  22736  cnclima  23406  iscncl  23407  cnclsi  23410  txcnmpt  23762  qtopval2  23834  qtopcn  23852  rnelfmlem  24090  fmfnfmlem4  24095  clssubg  24247  tgphaus  24255  tsmsgsum  24277  xmeter  24571  metustss  24689  metustexhalf  24694  restmetu  24708  rrxcph  25532  rrxsuppss  25543  mdegfval  26200  mdegleb  26202  mdegldg  26204  deg1mul3le  26255  plyeq0lem  26348  dgrcl  26371  dgrub  26372  dgrlb  26374  vieta1lem1  26452  suppovss  33007  pwrssmgc  33301  gsumfs2d  33362  gsumhashmul  33368  elrgspnlem4  33546  elrgspnsubrunlem1  33548  elrspunidl  33717  rprmdvdsprod  33805  1arithidom  33808  esplyfv1  33940  esplysply  33942  esplyfval3  33943  esplyfvaln  33945  dimkerim  33998  fedgmullem1  34000  lvecendof1f1o  34004  fldextrspunlsplem  34044  carsggect  34689  sibfof  34711  eulerpartlemsv2  34729  eulerpartlemsf  34730  eulerpartlemt  34742  eulerpartlemgu  34748  eulerpartlemgs2  34751  cvmliftmolem1  35754  cvmlift3lem6  35797  itg2addnclem  38303  keridl  38664  ismrcd1  43412  istopclsd  43414  pwfi2f1o  43806  sge0f1o  47079  smfsuplem1  47508