Theorem fssdm 6730

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3895  dom cdm 5650  ⟶wf 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896  df-fn 6542  df-f 6543

This theorem is used by:  fisuppfi  9367  wemapso  9549  wemapso2lem  9550  cantnfcl  9672  cantnfle  9676  cantnflt  9677  cantnff  9679  cantnfp1lem3  9685  cantnflem1b  9691  cantnflem1  9694  cantnflem3  9696  cnfcomlem  9704  cnfcom  9705  cnfcom3lem  9708  cnfcom3  9709  fin1a2lem7  10488  isercolllem2  15839  isercolllem3  15840  fsumss  15897  fprodss  16121  vdwlem1  17165  vdwlem5  17169  vdwlem6  17170  ghmpreima  19458  pmtrfconj  19686  gsumval3lem1  20125  gsumval3lem2  20126  gsumval3  20127  gsumzres  20129  gsumzcl2  20130  gsumzf1o  20132  gsumzmhm  20157  gsumzoppg  20164  gsum2d  20192  dpjidcl  20280  lmhmpreima  21329  rhmpreimaidl  21577  gsumfsum  21746  regsumsupp  21934  frlmlbs  22109  mplcoe1  22352  mplcoe5  22355  psr1baslem  22509  mdetdiaglem  22919  cnclima  23592  iscncl  23593  cnclsi  23596  txcnmpt  23949  qtopval2  24021  qtopcn  24039  rnelfmlem  24277  fmfnfmlem4  24282  clssubg  24434  tgphaus  24442  tsmsgsum  24464  xmeter  24758  metustss  24876  metustexhalf  24881  restmetu  24895  rrxcph  25719  rrxsuppss  25730  mdegfval  26386  mdegleb  26388  mdegldg  26390  deg1mul3le  26441  plyeq0lem  26535  dgrcl  26558  dgrub  26559  dgrlb  26561  vieta1lem1  26639  suppovss  33322  pwrssmgc  33608  gsumfs2d  33669  gsumhashmul  33675  elrgspnlem4  33853  elrgspnsubrunlem1  33855  elrspunidl  34025  rprmdvdsprod  34113  1arithidom  34116  esplyfv1  34248  esplysply  34250  esplyfval3  34251  esplyfvaln  34253  dimkerim  34306  fedgmullem1  34308  lvecendof1f1o  34312  fldextrspunlsplem  34352  carsggect  34997  sibfof  35019  eulerpartlemsv2  35037  eulerpartlemsf  35038  eulerpartlemt  35050  eulerpartlemgu  35056  eulerpartlemgs2  35059  cvmliftmolem1  36133  cvmlift3lem6  36176  itg2addnclem  38683  keridl  39060  ismrcd1  43803  istopclsd  43805  pwfi2f1o  44192  sge0f1o  47486  smfsuplem1  47915