Theorem fssdm 6723

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

Syntax hints:   → wi 4   ⊆ wss 3913  dom cdm 5659  ⟶wf 6529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930  df-fn 6536  df-f 6537

This theorem is referenced by:  fisuppfi  9327  wemapso  9509  wemapso2lem  9510  cantnfcl  9632  cantnfle  9636  cantnflt  9637  cantnff  9639  cantnfp1lem3  9645  cantnflem1b  9651  cantnflem1  9654  cantnflem3  9656  cnfcomlem  9664  cnfcom  9665  cnfcom3lem  9668  cnfcom3  9669  fin1a2lem7  10386  isercolllem2  15713  isercolllem3  15714  fsumss  15772  fprodss  15998  vdwlem1  17037  vdwlem5  17041  vdwlem6  17042  ghmpreima  19304  pmtrfconj  19532  gsumval3lem1  19971  gsumval3lem2  19972  gsumval3  19973  gsumzres  19975  gsumzcl2  19976  gsumzf1o  19978  gsumzmhm  20003  gsumzoppg  20010  gsum2d  20038  dpjidcl  20126  lmhmpreima  21143  rhmpreimaidl  21383  gsumfsum  21549  regsumsupp  21737  frlmlbs  21912  mplcoe1  22153  mplcoe5  22156  psr1baslem  22310  mdetdiaglem  22720  cnclima  23390  iscncl  23391  cnclsi  23394  txcnmpt  23746  qtopval2  23818  qtopcn  23836  rnelfmlem  24074  fmfnfmlem4  24079  clssubg  24231  tgphaus  24239  tsmsgsum  24261  xmeter  24555  metustss  24673  metustexhalf  24678  restmetu  24692  rrxcph  25516  rrxsuppss  25527  mdegfval  26184  mdegleb  26186  mdegldg  26188  deg1mul3le  26239  plyeq0lem  26332  dgrcl  26355  dgrub  26356  dgrlb  26358  vieta1lem1  26436  suppovss  32963  pwrssmgc  33257  gsumfs2d  33318  gsumhashmul  33324  elrgspnlem4  33502  elrgspnsubrunlem1  33504  elrspunidl  33676  rprmdvdsprod  33765  1arithidom  33768  esplyfv1  33900  esplysply  33902  esplyfval3  33903  esplyfvaln  33905  dimkerim  33958  fedgmullem1  33960  lvecendof1f1o  33964  fldextrspunlsplem  34004  carsggect  34649  sibfof  34671  eulerpartlemsv2  34689  eulerpartlemsf  34690  eulerpartlemt  34702  eulerpartlemgu  34708  eulerpartlemgs2  34711  cvmliftmolem1  35668  cvmlift3lem6  35711  itg2addnclem  38205  keridl  38566  ismrcd1  43314  istopclsd  43316  pwfi2f1o  43708  sge0f1o  46981  smfsuplem1  47410