Theorem fssdm 6689

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

Syntax hints:   → wi 4   ⊆ wss 3911  dom cdm 5631  ⟶wf 6495

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 3928  df-fn 6502  df-f 6503

This theorem is referenced by:  fisuppfi  9298  wemapso  9480  wemapso2lem  9481  cantnfcl  9596  cantnfle  9600  cantnflt  9601  cantnff  9603  cantnfp1lem3  9609  cantnflem1b  9615  cantnflem1  9618  cantnflem3  9620  cnfcomlem  9628  cnfcom  9629  cnfcom3lem  9632  cnfcom3  9633  fin1a2lem7  10335  isercolllem2  15608  isercolllem3  15609  fsumss  15667  fprodss  15890  vdwlem1  16928  vdwlem5  16932  vdwlem6  16933  ghmpreima  19146  pmtrfconj  19372  gsumval3lem1  19811  gsumval3lem2  19812  gsumval3  19813  gsumzres  19815  gsumzcl2  19816  gsumzf1o  19818  gsumzmhm  19843  gsumzoppg  19850  gsum2d  19878  dpjidcl  19966  lmhmpreima  20931  rhmpreimaidl  21163  gsumfsum  21327  regsumsupp  21507  frlmlbs  21682  mplcoe1  21920  mplcoe5  21923  psr1baslem  22045  mdetdiaglem  22461  cnclima  23131  iscncl  23132  cnclsi  23135  txcnmpt  23487  qtopval2  23559  qtopcn  23577  rnelfmlem  23815  fmfnfmlem4  23820  clssubg  23972  tgphaus  23980  tsmsgsum  24002  xmeter  24297  metustss  24415  metustexhalf  24420  restmetu  24434  rrxcph  25268  rrxsuppss  25279  mdegfval  25943  mdegleb  25945  mdegldg  25947  deg1mul3le  25998  plyeq0lem  26091  dgrcl  26114  dgrub  26115  dgrlb  26117  vieta1lem1  26194  suppovss  32577  pwrssmgc  32899  gsumfs2d  32968  gsumhashmul  32974  elrgspnlem4  33169  elrgspnsubrunlem1  33171  elrspunidl  33372  rprmdvdsprod  33478  1arithidom  33481  dimkerim  33596  fedgmullem1  33598  lvecendof1f1o  33602  fldextrspunlsplem  33641  carsggect  34282  sibfof  34304  eulerpartlemsv2  34322  eulerpartlemsf  34323  eulerpartlemt  34335  eulerpartlemgu  34341  eulerpartlemgs2  34344  cvmliftmolem1  35241  cvmlift3lem6  35284  itg2addnclem  37638  keridl  37999  ismrcd1  42659  istopclsd  42661  pwfi2f1o  43058  sge0f1o  46353  smfsuplem1  46782