Theorem fssdm 6707

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

Syntax hints:   → wi 4   ⊆ wss 3914  dom cdm 5638  ⟶wf 6507

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 3931  df-fn 6514  df-f 6515

This theorem is referenced by:  fisuppfi  9322  wemapso  9504  wemapso2lem  9505  cantnfcl  9620  cantnfle  9624  cantnflt  9625  cantnff  9627  cantnfp1lem3  9633  cantnflem1b  9639  cantnflem1  9642  cantnflem3  9644  cnfcomlem  9652  cnfcom  9653  cnfcom3lem  9656  cnfcom3  9657  fin1a2lem7  10359  isercolllem2  15632  isercolllem3  15633  fsumss  15691  fprodss  15914  vdwlem1  16952  vdwlem5  16956  vdwlem6  16957  ghmpreima  19170  pmtrfconj  19396  gsumval3lem1  19835  gsumval3lem2  19836  gsumval3  19837  gsumzres  19839  gsumzcl2  19840  gsumzf1o  19842  gsumzmhm  19867  gsumzoppg  19874  gsum2d  19902  dpjidcl  19990  lmhmpreima  20955  rhmpreimaidl  21187  gsumfsum  21351  regsumsupp  21531  frlmlbs  21706  mplcoe1  21944  mplcoe5  21947  psr1baslem  22069  mdetdiaglem  22485  cnclima  23155  iscncl  23156  cnclsi  23159  txcnmpt  23511  qtopval2  23583  qtopcn  23601  rnelfmlem  23839  fmfnfmlem4  23844  clssubg  23996  tgphaus  24004  tsmsgsum  24026  xmeter  24321  metustss  24439  metustexhalf  24444  restmetu  24458  rrxcph  25292  rrxsuppss  25303  mdegfval  25967  mdegleb  25969  mdegldg  25971  deg1mul3le  26022  plyeq0lem  26115  dgrcl  26138  dgrub  26139  dgrlb  26141  vieta1lem1  26218  suppovss  32604  pwrssmgc  32926  gsumfs2d  32995  gsumhashmul  33001  elrgspnlem4  33196  elrgspnsubrunlem1  33198  elrspunidl  33399  rprmdvdsprod  33505  1arithidom  33508  dimkerim  33623  fedgmullem1  33625  lvecendof1f1o  33629  fldextrspunlsplem  33668  carsggect  34309  sibfof  34331  eulerpartlemsv2  34349  eulerpartlemsf  34350  eulerpartlemt  34362  eulerpartlemgu  34368  eulerpartlemgs2  34371  cvmliftmolem1  35268  cvmlift3lem6  35311  itg2addnclem  37665  keridl  38026  ismrcd1  42686  istopclsd  42688  pwfi2f1o  43085  sge0f1o  46380  smfsuplem1  46809