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 3978	1 ⊢ (𝜑 → 𝐷 ⊆ 𝐴)

Syntax hints:   → wi 4   ⊆ wss 3903  dom cdm 5632  ⟶wf 6496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920  df-fn 6503  df-f 6504

This theorem is referenced by:  fisuppfi  9286  wemapso  9468  wemapso2lem  9469  cantnfcl  9588  cantnfle  9592  cantnflt  9593  cantnff  9595  cantnfp1lem3  9601  cantnflem1b  9607  cantnflem1  9610  cantnflem3  9612  cnfcomlem  9620  cnfcom  9621  cnfcom3lem  9624  cnfcom3  9625  fin1a2lem7  10328  isercolllem2  15601  isercolllem3  15602  fsumss  15660  fprodss  15883  vdwlem1  16921  vdwlem5  16925  vdwlem6  16926  ghmpreima  19179  pmtrfconj  19407  gsumval3lem1  19846  gsumval3lem2  19847  gsumval3  19848  gsumzres  19850  gsumzcl2  19851  gsumzf1o  19853  gsumzmhm  19878  gsumzoppg  19885  gsum2d  19913  dpjidcl  20001  lmhmpreima  21012  rhmpreimaidl  21244  gsumfsum  21401  regsumsupp  21589  frlmlbs  21764  mplcoe1  22004  mplcoe5  22007  psr1baslem  22137  mdetdiaglem  22554  cnclima  23224  iscncl  23225  cnclsi  23228  txcnmpt  23580  qtopval2  23652  qtopcn  23670  rnelfmlem  23908  fmfnfmlem4  23913  clssubg  24065  tgphaus  24073  tsmsgsum  24095  xmeter  24389  metustss  24507  metustexhalf  24512  restmetu  24526  rrxcph  25360  rrxsuppss  25371  mdegfval  26035  mdegleb  26037  mdegldg  26039  deg1mul3le  26090  plyeq0lem  26183  dgrcl  26206  dgrub  26207  dgrlb  26209  vieta1lem1  26286  suppovss  32770  pwrssmgc  33092  gsumfs2d  33154  gsumhashmul  33160  elrgspnlem4  33338  elrgspnsubrunlem1  33340  elrspunidl  33520  rprmdvdsprod  33626  1arithidom  33629  esplyfv1  33745  esplysply  33747  esplyfval3  33748  esplyfvaln  33750  dimkerim  33804  fedgmullem1  33806  lvecendof1f1o  33810  fldextrspunlsplem  33850  carsggect  34495  sibfof  34517  eulerpartlemsv2  34535  eulerpartlemsf  34536  eulerpartlemt  34548  eulerpartlemgu  34554  eulerpartlemgs2  34557  cvmliftmolem1  35494  cvmlift3lem6  35537  itg2addnclem  37919  keridl  38280  ismrcd1  43052  istopclsd  43054  pwfi2f1o  43450  sge0f1o  46737  smfsuplem1  47166