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

Theorem ressbas2 16550
Description: Base set of a structure restriction. (Contributed by Mario Carneiro, 2-Dec-2014.)
Hypotheses
Ref Expression
ressbas.r 𝑅 = (𝑊s 𝐴)
ressbas.b 𝐵 = (Base‘𝑊)
Assertion
Ref Expression
ressbas2 (𝐴𝐵𝐴 = (Base‘𝑅))

Proof of Theorem ressbas2
StepHypRef Expression
1 df-ss 3901 . . 3 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
21biimpi 219 . 2 (𝐴𝐵 → (𝐴𝐵) = 𝐴)
3 ressbas.b . . . . 5 𝐵 = (Base‘𝑊)
43fvexi 6663 . . . 4 𝐵 ∈ V
54ssex 5192 . . 3 (𝐴𝐵𝐴 ∈ V)
6 ressbas.r . . . 4 𝑅 = (𝑊s 𝐴)
76, 3ressbas 16549 . . 3 (𝐴 ∈ V → (𝐴𝐵) = (Base‘𝑅))
85, 7syl 17 . 2 (𝐴𝐵 → (𝐴𝐵) = (Base‘𝑅))
92, 8eqtr3d 2838 1 (𝐴𝐵𝐴 = (Base‘𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2112  Vcvv 3444  cin 3883  wss 3884  cfv 6328  (class class class)co 7139  Basecbs 16478  s cress 16479
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-cnex 10586  ax-1cn 10588  ax-addcl 10590
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-nn 11630  df-ndx 16481  df-slot 16482  df-base 16484  df-sets 16485  df-ress 16486
This theorem is referenced by:  rescbas  17094  fullresc  17116  resssetc  17347  yoniso  17530  issstrmgm  17858  gsumress  17887  issubmnd  17933  ress0g  17934  submnd0  17935  submbas  17974  resmhm  17980  resgrpplusfrn  18112  subgbas  18278  issubg2  18289  resghm  18369  symgbas  18494  submod  18689  cntrcmnd  18958  ringidss  19326  unitgrpbas  19415  isdrng2  19508  drngmcl  19511  drngid2  19514  isdrngd  19523  cntzsdrg  19577  subdrgint  19578  primefld  19580  islss3  19727  lsslss  19729  lsslsp  19783  reslmhm  19820  xrs1mnd  20132  xrs10  20133  xrs1cmn  20134  xrge0subm  20135  xrge0cmn  20136  cnmsubglem  20157  nn0srg  20164  rge0srg  20165  zringbas  20172  expghm  20192  cnmsgnbas  20270  psgnghm  20272  rebase  20298  dsmmbase  20427  dsmmval2  20428  lsslindf  20522  lsslinds  20523  islinds3  20526  resspsrbas  20656  mplbas  20670  ressmplbas  20699  evlssca  20764  mpfconst  20776  mpfind  20782  ply1bas  20827  ressply1bas  20861  evls1sca  20950  m2cpmrngiso  21366  ressusp  22874  imasdsf1olem  22983  xrge0gsumle  23441  xrge0tsms  23442  cmssmscld  23957  cmsss  23958  minveclem3a  24034  efabl  25145  efsubm  25146  qrngbas  26206  ressplusf  30666  ressnm  30667  ressprs  30671  ressmulgnn  30720  ressmulgnn0  30721  xrge0tsmsd  30745  ress1r  30914  xrge0slmod  30971  drgextlsp  31084  lssdimle  31094  lbslsat  31102  dimkerim  31111  fedgmullem1  31113  fedgmullem2  31114  fedgmul  31115  rspecbas  31218  prsssdm  31268  ordtrestNEW  31272  ordtrest2NEW  31274  xrge0iifmhm  31290  esumpfinvallem  31441  sitgaddlemb  31714  prdsbnd2  35226  cnpwstotbnd  35228  repwsmet  35265  rrnequiv  35266  lcdvbase  38882  selvval2lem4  39418  islssfg  40001  lnmlsslnm  40012  pwssplit4  40020  deg1mhm  40138  gsumge0cl  42997  sge0tsms  43006  cnfldsrngbas  44376  issubmgm2  44397  submgmbas  44403  resmgmhm  44405  amgmlemALT  45318
  Copyright terms: Public domain W3C validator