Theorem fssdm 6729

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3906  dom cdm 5663  ⟶wf 6536

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 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ss 3923  df-fn 6543  df-f 6544

This theorem is used by:  fisuppfi  9334  wemapso  9516  wemapso2lem  9517  cantnfcl  9639  cantnfle  9643  cantnflt  9644  cantnff  9646  cantnfp1lem3  9652  cantnflem1b  9658  cantnflem1  9661  cantnflem3  9663  cnfcomlem  9671  cnfcom  9672  cnfcom3lem  9675  cnfcom3  9676  fin1a2lem7  10401  isercolllem2  15736  isercolllem3  15737  fsumss  15794  fprodss  16020  vdwlem1  17058  vdwlem5  17062  vdwlem6  17063  ghmpreima  19331  pmtrfconj  19559  gsumval3lem1  19998  gsumval3lem2  19999  gsumval3  20000  gsumzres  20002  gsumzcl2  20003  gsumzf1o  20005  gsumzmhm  20030  gsumzoppg  20037  gsum2d  20065  dpjidcl  20153  lmhmpreima  21198  rhmpreimaidl  21445  gsumfsum  21613  regsumsupp  21801  frlmlbs  21976  mplcoe1  22217  mplcoe5  22220  psr1baslem  22374  mdetdiaglem  22784  cnclima  23454  iscncl  23455  cnclsi  23458  txcnmpt  23810  qtopval2  23882  qtopcn  23900  rnelfmlem  24138  fmfnfmlem4  24143  clssubg  24295  tgphaus  24303  tsmsgsum  24325  xmeter  24619  metustss  24737  metustexhalf  24742  restmetu  24756  rrxcph  25580  rrxsuppss  25591  mdegfval  26248  mdegleb  26250  mdegldg  26252  deg1mul3le  26303  plyeq0lem  26396  dgrcl  26419  dgrub  26420  dgrlb  26422  vieta1lem1  26500  suppovss  33055  pwrssmgc  33343  gsumfs2d  33404  gsumhashmul  33410  elrgspnlem4  33588  elrgspnsubrunlem1  33590  elrspunidl  33759  rprmdvdsprod  33847  1arithidom  33850  esplyfv1  33982  esplysply  33984  esplyfval3  33985  esplyfvaln  33987  dimkerim  34040  fedgmullem1  34042  lvecendof1f1o  34046  fldextrspunlsplem  34086  carsggect  34732  sibfof  34754  eulerpartlemsv2  34772  eulerpartlemsf  34773  eulerpartlemt  34785  eulerpartlemgu  34791  eulerpartlemgs2  34794  cvmliftmolem1  35786  cvmlift3lem6  35829  itg2addnclem  38355  keridl  38716  ismrcd1  43462  istopclsd  43464  pwfi2f1o  43856  sge0f1o  47129  smfsuplem1  47558