Theorem ressbas2 17199

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 3901	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2	1	biimpi 217	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = 𝐴)
3		ressbas.b	. . . . 5 ⊢ 𝐵 = (Base‘𝑊)
4	3	fvexi 6841	. . . 4 ⊢ 𝐵 ∈ V
5	4	ssex 5249	. . 3 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
6		ressbas.r	. . . 4 ⊢ 𝑅 = (𝑊 ↾s 𝐴)
7	6, 3	ressbas 17197	. . 3 ⊢ (𝐴 ∈ V → (𝐴 ∩ 𝐵) = (Base‘𝑅))
8	5, 7	syl 17	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = (Base‘𝑅))
9	2, 8	eqtr3d 2776	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘𝑅))

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  Vcvv 3431   ∩ cin 3882   ⊆ wss 3883  ‘cfv 6485  (class class class)co 7356  Basecbs 17170   ↾_s cress 17191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-cnex 11085  ax-1cn 11087  ax-addcl 11089

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-nn 12166  df-sets 17125  df-slot 17143  df-ndx 17155  df-base 17171  df-ress 17192

This theorem is referenced by:  rescbas  17787  fullresc  17809  resssetc  18050  yoniso  18242  issstrmgm  18612  gsumress  18641  issubmgm2  18662  submgmbas  18668  resmgmhm  18670  issubmnd  18720  ress0g  18721  submnd0  18722  submbas  18773  resmhm  18779  resgrpplusfrn  18917  ressmulgnn  19043  ressmulgnn0  19044  ressmulgnnd  19045  subgbas  19097  issubg2  19108  resghm  19198  symgbas  19338  finodsubmsubg  19533  submod  19535  cntrcmnd  19808  ringidss  20249  unitgrpbas  20353  isdrng2  20715  drngmclOLD  20723  drngid2  20724  isdrngd  20737  isdrngdOLD  20739  sdrgbas  20766  cntzsdrg  20774  subdrgint  20775  primefld  20777  islss3  20949  lsslss  20951  lsslsp  21005  reslmhm  21042  2idlbas  21256  rng2idl1cntr  21298  cnmsubglem  21405  nn0srg  21412  rge0srg  21413  xrs1mnd  21415  xrs10  21416  xrs1cmn  21417  xrge0subm  21418  xrge0cmn  21419  zringbas  21428  expghm  21450  fermltlchr  21504  cnmsgnbas  21553  psgnghm  21555  rebase  21581  dsmmbase  21710  dsmmval2  21711  lsslindf  21805  lsslinds  21806  islinds3  21809  resspsrbas  21948  mplbas  21964  ressmplbas  22003  evlssca  22070  mpfconst  22085  mpfind  22091  ply1bas  22180  ressply1bas  22213  evls1sca  22309  evls1fpws  22355  evls1vsca  22359  asclply1subcl  22360  evls1maplmhm  22363  m2cpmrngiso  22741  ressusp  24247  imasdsf1olem  24356  xrge0gsumle  24817  xrge0tsms  24818  cmssmscld  25335  cmsss  25336  minveclem3a  25412  efabl  26532  efsubm  26533  qrngbas  27600  ressplusf  33042  ressnm  33043  ressprs  33045  subgmulgcld  33124  ressmulgnn0d  33125  xrge0tsmsd  33154  ress1r  33314  subrdom  33366  subsdrg  33382  idomsubr  33393  xrge0slmod  33431  znfermltl  33449  ressply1evls1  33648  ressasclcl  33654  resssra  33771  drgextlsp  33778  lssdimle  33792  lbslsat  33800  ply1degltdimlem  33806  ply1degltdim  33807  dimkerim  33811  fedgmullem1  33813  fedgmullem2  33814  fedgmul  33815  dimlssid  33816  lvecendof1f1o  33817  sdrgfldext  33834  fldsdrgfldext  33845  fldsdrgfldext2  33846  fldgenfldext  33852  evls1fldgencl  33854  fldextrspunlsplem  33857  fldextrspunlsp  33858  fldextrspunlem1  33859  fldextrspunfld  33860  fldextrspundgle  33862  fldextrspundgdvdslem  33864  fldextrspundgdvds  33865  0ringirng  33873  extdgfialglem1  33876  extdgfialglem2  33877  algextdeglem3  33903  algextdeglem4  33904  algextdeglem8  33908  rtelextdg2lem  33910  rtelextdg2  33911  constrext2chnlem  33934  2sqr3minply  33964  rspecbas  34049  prsssdm  34101  ordtrestNEW  34105  ordtrest2NEW  34107  xrge0iifmhm  34123  esumpfinvallem  34258  sitgaddlemb  34532  prdsbnd2  38162  cnpwstotbnd  38164  repwsmet  38201  rrnequiv  38202  lcdvbase  42085  primrootsunit1  42582  primrootscoprmpow  42584  primrootscoprbij  42587  aks6d1c6lem4  42658  aks6d1c6isolem2  42660  aks6d1c6lem5  42662  aks5lem7  42685  islssfg  43515  lnmlsslnm  43526  pwssplit4  43534  deg1mhm  43645  gsumge0cl  46814  sge0tsms  46823  cnfldsrngbas  48652  amgmlemALT  50293