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

Theorem ressid 15916
Description: Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
Hypothesis
Ref Expression
ressid.1 𝐵 = (Base‘𝑊)
Assertion
Ref Expression
ressid (𝑊𝑋 → (𝑊s 𝐵) = 𝑊)

Proof of Theorem ressid
StepHypRef Expression
1 ssid 3616 . 2 𝐵𝐵
2 ressid.1 . . 3 𝐵 = (Base‘𝑊)
3 fvex 6188 . . 3 (Base‘𝑊) ∈ V
42, 3eqeltri 2695 . 2 𝐵 ∈ V
5 eqid 2620 . . 3 (𝑊s 𝐵) = (𝑊s 𝐵)
65, 2ressid2 15909 . 2 ((𝐵𝐵𝑊𝑋𝐵 ∈ V) → (𝑊s 𝐵) = 𝑊)
71, 4, 6mp3an13 1413 1 (𝑊𝑋 → (𝑊s 𝐵) = 𝑊)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  wcel 1988  Vcvv 3195  wss 3567  cfv 5876  (class class class)co 6635  Basecbs 15838  s cress 15839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-iota 5839  df-fun 5878  df-fv 5884  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-ress 15846
This theorem is referenced by:  ressval3d  15918  submid  17332  subgid  17577  gaid2  17717  subrgid  18763  rlmval2  19175  rlmsca  19181  rlmsca2  19182  evlrhm  19506  evlsscasrng  19507  evlsvarsrng  19509  evl1sca  19679  evl1var  19681  evls1scasrng  19684  evls1varsrng  19685  pf1ind  19700  evl1gsumadd  19703  evl1varpw  19706  pjff  20037  dsmmfi  20063  frlmip  20098  cnstrcvs  22922  cncvs  22926  rlmbn  23138  ishl2  23147  rrxprds  23158  dchrptlem2  24971  lnmfg  37471  lmhmfgsplit  37475  pwslnmlem2  37482  submgmid  41558
  Copyright terms: Public domain W3C validator