Theorem fssdm 6705

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

Syntax hints:   → wi 4   ⊆ wss 3902  dom cdm 5643  ⟶wf 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3919  df-fn 6518  df-f 6519

This theorem is referenced by:  fisuppfi  9310  wemapso  9492  wemapso2lem  9493  cantnfcl  9615  cantnfle  9619  cantnflt  9620  cantnff  9622  cantnfp1lem3  9628  cantnflem1b  9634  cantnflem1  9637  cantnflem3  9639  cnfcomlem  9647  cnfcom  9648  cnfcom3lem  9651  cnfcom3  9652  fin1a2lem7  10356  isercolllem2  15683  isercolllem3  15684  fsumss  15742  fprodss  15968  vdwlem1  17007  vdwlem5  17011  vdwlem6  17012  ghmpreima  19268  pmtrfconj  19496  gsumval3lem1  19935  gsumval3lem2  19936  gsumval3  19937  gsumzres  19939  gsumzcl2  19940  gsumzf1o  19942  gsumzmhm  19967  gsumzoppg  19974  gsum2d  20002  dpjidcl  20090  lmhmpreima  21102  rhmpreimaidl  21334  gsumfsum  21473  regsumsupp  21661  frlmlbs  21836  mplcoe1  22077  mplcoe5  22080  psr1baslem  22234  mdetdiaglem  22645  cnclima  23315  iscncl  23316  cnclsi  23319  txcnmpt  23671  qtopval2  23743  qtopcn  23761  rnelfmlem  23999  fmfnfmlem4  24004  clssubg  24156  tgphaus  24164  tsmsgsum  24186  xmeter  24480  metustss  24598  metustexhalf  24603  restmetu  24617  rrxcph  25441  rrxsuppss  25452  mdegfval  26109  mdegleb  26111  mdegldg  26113  deg1mul3le  26164  plyeq0lem  26257  dgrcl  26280  dgrub  26281  dgrlb  26283  vieta1lem1  26361  suppovss  32843  pwrssmgc  33138  gsumfs2d  33201  gsumhashmul  33207  elrgspnlem4  33386  elrgspnsubrunlem1  33388  elrspunidl  33574  rprmdvdsprod  33690  1arithidom  33693  esplyfv1  33826  esplysply  33828  esplyfval3  33829  esplyfvaln  33831  dimkerim  33884  fedgmullem1  33886  lvecendof1f1o  33890  fldextrspunlsplem  33930  carsggect  34575  sibfof  34597  eulerpartlemsv2  34615  eulerpartlemsf  34616  eulerpartlemt  34628  eulerpartlemgu  34634  eulerpartlemgs2  34637  cvmliftmolem1  35591  cvmlift3lem6  35634  itg2addnclem  38130  keridl  38491  ismrcd1  43239  istopclsd  43241  pwfi2f1o  43633  sge0f1o  46916  smfsuplem1  47345