MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fssdm Structured version   Visualization version   GIF version

Theorem fssdm 6503
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
StepHypRef Expression
1 fssdm.d . 2 𝐷 ⊆ dom 𝐹
2 fssdm.f . . 3 (𝜑𝐹:𝐴𝐵)
32fdmd 6496 . 2 (𝜑 → dom 𝐹 = 𝐴)
41, 3sseqtrid 3995 1 (𝜑𝐷𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3910  dom cdm 5528  wf 6324
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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-v 3473  df-in 3917  df-ss 3927  df-fn 6331  df-f 6332
This theorem is referenced by:  fisuppfi  8817  wemapso  8991  wemapso2lem  8992  cantnfcl  9106  cantnfle  9110  cantnflt  9111  cantnff  9113  cantnfp1lem3  9119  cantnflem1b  9125  cantnflem1  9128  cantnflem3  9130  cnfcomlem  9138  cnfcom  9139  cnfcom3lem  9142  cnfcom3  9143  fin1a2lem7  9805  isercolllem2  15001  isercolllem3  15002  fsumss  15061  fprodss  15281  vdwlem1  16294  vdwlem5  16298  vdwlem6  16299  ghmpreima  18359  pmtrfconj  18573  gsumval3lem1  19004  gsumval3lem2  19005  gsumval3  19006  gsumzres  19008  gsumzcl2  19009  gsumzf1o  19011  gsumzmhm  19036  gsumzoppg  19043  gsum2d  19071  dpjidcl  19159  lmhmpreima  19796  mplcoe1  20222  mplcoe5  20225  psr1baslem  20329  gsumfsum  20588  regsumsupp  20742  frlmlbs  20917  mdetdiaglem  21183  cnclima  21852  iscncl  21853  cnclsi  21856  txcnmpt  22208  qtopval2  22280  qtopcn  22298  rnelfmlem  22536  fmfnfmlem4  22541  clssubg  22693  tgphaus  22701  tsmsgsum  22723  xmeter  23019  metustss  23137  metustexhalf  23142  restmetu  23156  rrxcph  23975  rrxsuppss  23986  mdegfval  24642  mdegleb  24644  mdegldg  24646  deg1mul3le  24696  plyeq0lem  24786  dgrcl  24809  dgrub  24810  dgrlb  24812  vieta1lem1  24885  suppovss  30413  pwrssmgc  30667  dimkerim  31034  fedgmullem1  31036  carsggect  31584  sibfof  31606  eulerpartlemsv2  31624  eulerpartlemsf  31625  eulerpartlemt  31637  eulerpartlemgu  31643  eulerpartlemgs2  31646  cvmliftmolem1  32536  cvmlift3lem6  32579  itg2addnclem  34994  keridl  35356  ismrcd1  39450  istopclsd  39452  pwfi2f1o  39851  sge0f1o  42844  smfsuplem1  43265
  Copyright terms: Public domain W3C validator