Theorem fssdm 6742

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

Syntax hints:   → wi 4   ⊆ wss 3944  dom cdm 5678  ⟶wf 6545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-ss 3961  df-fn 6552  df-f 6553

This theorem is referenced by:  fisuppfi  9397  wemapso  9576  wemapso2lem  9577  cantnfcl  9692  cantnfle  9696  cantnflt  9697  cantnff  9699  cantnfp1lem3  9705  cantnflem1b  9711  cantnflem1  9714  cantnflem3  9716  cnfcomlem  9724  cnfcom  9725  cnfcom3lem  9728  cnfcom3  9729  fin1a2lem7  10431  isercolllem2  15648  isercolllem3  15649  fsumss  15707  fprodss  15928  vdwlem1  16953  vdwlem5  16957  vdwlem6  16958  ghmpreima  19201  pmtrfconj  19433  gsumval3lem1  19872  gsumval3lem2  19873  gsumval3  19874  gsumzres  19876  gsumzcl2  19877  gsumzf1o  19879  gsumzmhm  19904  gsumzoppg  19911  gsum2d  19939  dpjidcl  20027  lmhmpreima  20945  rhmpreimaidl  21184  gsumfsum  21384  regsumsupp  21571  frlmlbs  21748  mplcoe1  21997  mplcoe5  22000  psr1baslem  22127  mdetdiaglem  22544  cnclima  23216  iscncl  23217  cnclsi  23220  txcnmpt  23572  qtopval2  23644  qtopcn  23662  rnelfmlem  23900  fmfnfmlem4  23905  clssubg  24057  tgphaus  24065  tsmsgsum  24087  xmeter  24383  metustss  24504  metustexhalf  24509  restmetu  24523  rrxcph  25364  rrxsuppss  25375  mdegfval  26042  mdegleb  26044  mdegldg  26046  deg1mul3le  26097  plyeq0lem  26189  dgrcl  26212  dgrub  26213  dgrlb  26215  vieta1lem1  26290  suppovss  32547  pwrssmgc  32816  gsumhashmul  32860  elrspunidl  33240  rprmdvdsprod  33346  1arithidom  33349  dimkerim  33456  fedgmullem1  33458  carsggect  34069  sibfof  34091  eulerpartlemsv2  34109  eulerpartlemsf  34110  eulerpartlemt  34122  eulerpartlemgu  34128  eulerpartlemgs2  34131  cvmliftmolem1  35022  cvmlift3lem6  35065  itg2addnclem  37275  keridl  37636  ismrcd1  42260  istopclsd  42262  pwfi2f1o  42662  sge0f1o  45908  smfsuplem1  46337