Theorem fssdmd 6714

Description: Expressing that a class is a subclass of the domain of a function expressed in maps-to notation, deduction form. (Contributed by AV, 21-Aug-2022.)

Hypotheses

Ref	Expression
fssdmd.f	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
fssdmd.d	⊢ (𝜑 → 𝐷 ⊆ dom 𝐹)

Assertion

Ref	Expression
fssdmd	⊢ (𝜑 → 𝐷 ⊆ 𝐴)

Proof of Theorem fssdmd

Step	Hyp	Ref	Expression
1		fssdmd.d	. 2 ⊢ (𝜑 → 𝐷 ⊆ dom 𝐹)
2		fssdmd.f	. . 3 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
3	2	fdmd 6706	. 2 ⊢ (𝜑 → dom 𝐹 = 𝐴)
4	1, 3	sseqtrd 3975	1 ⊢ (𝜑 → 𝐷 ⊆ 𝐴)

Syntax hints:   → wi 4   ⊆ wss 3907  dom cdm 5651  ⟶wf 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ss 3924  df-fn 6528  df-f 6529

This theorem is referenced by:  ordtypelem7  9474  vdwlem11  17039  gsumzoppg  20002  taylfvallem1  26474  taylply2  26485  taylply  26486  dvtaylp  26487  dvntaylp0  26489  taylthlem1  26490  taylthlem2  26491  tocyccntz  33372  omssubadd  34602