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

Theorem ressbas2 15699
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 3548 . . 3 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
21biimpi 204 . 2 (𝐴𝐵 → (𝐴𝐵) = 𝐴)
3 ressbas.b . . . . 5 𝐵 = (Base‘𝑊)
4 fvex 6093 . . . . 5 (Base‘𝑊) ∈ V
53, 4eqeltri 2678 . . . 4 𝐵 ∈ V
65ssex 4720 . . 3 (𝐴𝐵𝐴 ∈ V)
7 ressbas.r . . . 4 𝑅 = (𝑊s 𝐴)
87, 3ressbas 15698 . . 3 (𝐴 ∈ V → (𝐴𝐵) = (Base‘𝑅))
96, 8syl 17 . 2 (𝐴𝐵 → (𝐴𝐵) = (Base‘𝑅))
102, 9eqtr3d 2640 1 (𝐴𝐵𝐴 = (Base‘𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1975  Vcvv 3167  cin 3533  wss 3534  cfv 5785  (class class class)co 6522  Basecbs 15636  s cress 15637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584  ax-sep 4698  ax-nul 4707  ax-pow 4759  ax-pr 4823  ax-un 6819  ax-cnex 9843  ax-resscn 9844  ax-1cn 9845  ax-icn 9846  ax-addcl 9847  ax-addrcl 9848  ax-mulcl 9849  ax-mulrcl 9850  ax-i2m1 9855  ax-1ne0 9856  ax-rrecex 9859  ax-cnre 9860
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2456  df-mo 2457  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-ne 2776  df-ral 2895  df-rex 2896  df-reu 2897  df-rab 2899  df-v 3169  df-sbc 3397  df-csb 3494  df-dif 3537  df-un 3539  df-in 3541  df-ss 3548  df-pss 3550  df-nul 3869  df-if 4031  df-pw 4104  df-sn 4120  df-pr 4122  df-tp 4124  df-op 4126  df-uni 4362  df-iun 4446  df-br 4573  df-opab 4633  df-mpt 4634  df-tr 4670  df-eprel 4934  df-id 4938  df-po 4944  df-so 4945  df-fr 4982  df-we 4984  df-xp 5029  df-rel 5030  df-cnv 5031  df-co 5032  df-dm 5033  df-rn 5034  df-res 5035  df-ima 5036  df-pred 5578  df-ord 5624  df-on 5625  df-lim 5626  df-suc 5627  df-iota 5749  df-fun 5787  df-fn 5788  df-f 5789  df-f1 5790  df-fo 5791  df-f1o 5792  df-fv 5793  df-ov 6525  df-oprab 6526  df-mpt2 6527  df-om 6930  df-wrecs 7266  df-recs 7327  df-rdg 7365  df-nn 10863  df-ndx 15639  df-slot 15640  df-base 15641  df-sets 15642  df-ress 15643
This theorem is referenced by:  rescbas  16253  fullresc  16275  resssetc  16506  yoniso  16689  issstrmgm  17016  gsumress  17040  issubmnd  17082  ress0g  17083  submnd0  17084  submbas  17119  resmhm  17123  resgrpplusfrn  17200  subgbas  17362  issubg2  17373  resghm  17440  submod  17748  ringidss  18341  unitgrpbas  18430  isdrng2  18521  drngmcl  18524  drngid2  18527  isdrngd  18536  islss3  18721  lsslss  18723  lsslsp  18777  reslmhm  18814  issubassa  19086  resspsrbas  19177  mplbas  19191  ressmplbas  19218  evlssca  19284  mpfconst  19292  mpfind  19298  ply1bas  19327  ressply1bas  19361  evls1sca  19450  xrs1mnd  19544  xrs10  19545  xrs1cmn  19546  xrge0subm  19547  xrge0cmn  19548  cnmsubglem  19569  nn0srg  19576  rge0srg  19577  zringbas  19584  expghm  19603  cnmsgnbas  19683  psgnghm  19685  rebase  19711  dsmmbase  19835  dsmmval2  19836  lsslindf  19925  lsslinds  19926  islinds3  19929  m2cpmrngiso  20319  ressusp  21816  imasdsf1olem  21924  xrge0gsumle  22371  xrge0tsms  22372  cmsss  22867  minveclem3a  22918  efabl  24012  efsubm  24013  qrngbas  25020  ressplusf  28782  ressnm  28783  ressprs  28787  ressmulgnn  28815  ressmulgnn0  28816  xrge0tsmsd  28917  ress1r  28921  xrge0slmod  28976  prsssdm  29092  ordtrestNEW  29096  ordtrest2NEW  29098  xrge0iifmhm  29114  esumpfinvallem  29264  sitgaddlemb  29538  prdsbnd2  32562  cnpwstotbnd  32564  repwsmet  32601  rrnequiv  32602  lcdvbase  35698  islssfg  36456  lnmlsslnm  36467  pwssplit4  36475  cntzsdrg  36589  deg1mhm  36602  gsumge0cl  39063  sge0tsms  39072  cnfldsrngbas  41556  issubmgm2  41577  submgmbas  41583  resmgmhm  41585  amgmlemALT  42316
  Copyright terms: Public domain W3C validator