Theorem fssdm 6759

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3900  dom cdm 5658  ⟶wf 6562

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901  df-fn 6569  df-f 6570

This theorem is used by:  fisuppfi  9401  wemapso  9582  wemapso2lem  9583  cantnfcl  9705  cantnfle  9709  cantnflt  9710  cantnff  9712  cantnfp1lem3  9718  cantnflem1b  9724  cantnflem1  9727  cantnflem3  9729  cnfcomlem  9737  cnfcom  9738  cnfcom3lem  9741  cnfcom3  9742  fin1a2lem7  10523  isercolllem2  15877  isercolllem3  15878  fsumss  15935  fprodss  16159  vdwlem1  17203  vdwlem5  17207  vdwlem6  17208  ghmpreima  19502  pmtrfconj  19731  gsumval3lem1  20170  gsumval3lem2  20171  gsumval3  20172  gsumzres  20174  gsumzcl2  20175  gsumzf1o  20177  gsumzmhm  20202  gsumzoppg  20209  gsum2d  20237  dpjidcl  20325  lmhmpreima  21374  rhmpreimaidl  21622  gsumfsum  21794  regsumsupp  21983  frlmlbs  22158  mplcoe1  22401  mplcoe5  22404  psr1baslem  22558  mdetdiaglem  22968  cnclima  23641  iscncl  23642  cnclsi  23645  txcnmpt  23998  qtopval2  24070  qtopcn  24088  rnelfmlem  24326  fmfnfmlem4  24331  clssubg  24483  tgphaus  24491  tsmsgsum  24513  xmeter  24807  metustss  24925  metustexhalf  24930  restmetu  24944  rrxcph  25768  rrxsuppss  25779  mdegfval  26435  mdegleb  26437  mdegldg  26439  deg1mul3le  26490  plyeq0lem  26584  dgrcl  26607  dgrub  26608  dgrlb  26610  vieta1lem1  26688  suppovss  33371  pwrssmgc  33660  gsumfs2d  33721  gsumhashmul  33727  elrgspnlem4  33905  elrgspnsubrunlem1  33907  elrspunidl  34082  rprmdvdsprod  34170  1arithidom  34173  esplyfv1  34312  esplysply  34314  esplyfval3  34315  esplyfvaln  34317  dimkerim  34370  fedgmullem1  34372  lvecendof1f1o  34376  fldextrspunlsplem  34416  carsggect  35061  sibfof  35083  eulerpartlemsv2  35101  eulerpartlemsf  35102  eulerpartlemt  35114  eulerpartlemgu  35120  eulerpartlemgs2  35123  cvmliftmolem1  36254  cvmlift3lem6  36297  itg2addnclem  38857  keridl  39232  ismrcd1  43975  istopclsd  43977  pwfi2f1o  44364  sge0f1o  47665  smfsuplem1  48094