Theorem ressbas2 17265

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

Step	Hyp	Ref	Expression
1		dfss2 3920	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2	1	biimpi 218	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = 𝐴)
3		ressbas.b	. . . . 5 ⊢ 𝐵 = (Base‘𝑊)
4	3	fvexi 6876	. . . 4 ⊢ 𝐵 ∈ V
5	4	ssex 5274	. . 3 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
6		ressbas.r	. . . 4 ⊢ 𝑅 = (𝑊 ↾s 𝐴)
7	6, 3	ressbas 17263	. . 3 ⊢ (𝐴 ∈ V → (𝐴 ∩ 𝐵) = (Base‘𝑅))
8	5, 7	syl 17	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = (Base‘𝑅))
9	2, 8	eqtr3d 2798	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘𝑅))

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  Vcvv 3453   ∩ cin 3901   ⊆ wss 3902  ‘cfv 6516  (class class class)co 7391  Basecbs 17236   ↾_s cress 17257

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-cnex 11123  ax-1cn 11125  ax-addcl 11127

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-ov 7394  df-oprab 7395  df-mpo 7396  df-om 7842  df-2nd 7966  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-nn 12205  df-sets 17191  df-slot 17209  df-ndx 17221  df-base 17237  df-ress 17258

This theorem is referenced by:  rescbas  17853  fullresc  17875  resssetc  18116  yoniso  18308  issstrmgm  18678  gsumress  18707  issubmgm2  18728  submgmbas  18734  resmgmhm  18736  issubmnd  18786  ress0g  18787  submnd0  18788  submbas  18839  resmhm  18845  resgrpplusfrn  18983  ressmulgnn  19109  ressmulgnn0  19110  ressmulgnnd  19111  subgbas  19163  issubg2  19174  resghm  19263  symgbas  19403  finodsubmsubg  19598  submod  19600  cntrcmnd  19873  ringidss  20314  unitgrpbas  20418  isdrng2  20780  drngmclOLD  20788  drngid2  20789  isdrngd  20802  isdrngdOLD  20804  sdrgbas  20831  cntzsdrg  20839  subdrgint  20840  primefld  20842  islss3  21014  lsslss  21016  lsslsp  21070  reslmhm  21107  2idlbas  21321  rng2idl1cntr  21363  cnmsubglem  21470  nn0srg  21477  rge0srg  21478  xrs1mnd  21480  xrs10  21481  xrs1cmn  21482  xrge0subm  21483  xrge0cmn  21484  zringbas  21493  expghm  21515  fermltlchr  21569  cnmsgnbas  21618  psgnghm  21620  rebase  21646  dsmmbase  21775  dsmmval2  21776  lsslindf  21870  lsslinds  21871  islinds3  21874  resspsrbas  22013  mplbas  22029  ressmplbas  22068  evlssca  22135  mpfconst  22150  mpfind  22156  ply1bas  22245  ressply1bas  22278  evls1sca  22374  evls1fpws  22420  evls1vsca  22424  asclply1subcl  22425  evls1maplmhm  22428  m2cpmrngiso  22806  ressusp  24312  imasdsf1olem  24421  xrge0gsumle  24882  xrge0tsms  24883  cmssmscld  25400  cmsss  25401  minveclem3a  25477  efabl  26603  efsubm  26604  qrngbas  27671  ressplusf  33102  ressnm  33103  ressprs  33105  subgmulgcld  33184  ressmulgnn0d  33185  xrge0tsmsd  33214  ress1r  33374  subrdom  33430  subsdrg  33446  idomsubr  33457  xrge0slmod  33495  znfermltl  33513  ressply1evls1  33722  ressasclcl  33728  resssra  33845  drgextlsp  33852  lssdimle  33866  lbslsat  33874  ply1degltdimlem  33880  ply1degltdim  33881  dimkerim  33885  fedgmullem1  33887  fedgmullem2  33888  fedgmul  33889  dimlssid  33890  lvecendof1f1o  33891  sdrgfldext  33908  fldsdrgfldext  33919  fldsdrgfldext2  33920  fldgenfldext  33926  evls1fldgencl  33928  fldextrspunlsplem  33931  fldextrspunlsp  33932  fldextrspunlem1  33933  fldextrspunfld  33934  fldextrspundgle  33936  fldextrspundgdvdslem  33938  fldextrspundgdvds  33939  0ringirng  33947  extdgfialglem1  33950  extdgfialglem2  33951  algextdeglem3  33977  algextdeglem4  33978  algextdeglem8  33982  rtelextdg2lem  33984  rtelextdg2  33985  constrext2chnlem  34008  2sqr3minply  34038  rspecbas  34123  prsssdm  34175  ordtrestNEW  34179  ordtrest2NEW  34181  xrge0iifmhm  34197  esumpfinvallem  34332  sitgaddlemb  34606  prdsbnd2  38255  cnpwstotbnd  38257  repwsmet  38294  rrnequiv  38295  lcdvbase  42178  primrootsunit1  42675  primrootscoprmpow  42677  primrootscoprbij  42680  aks6d1c6lem4  42751  aks6d1c6isolem2  42753  aks6d1c6lem5  42755  aks5lem7  42778  islssfg  43608  lnmlsslnm  43619  pwssplit4  43627  deg1mhm  43738  gsumge0cl  46906  sge0tsms  46915  cnfldsrngbas  48744  amgmlemALT  50385