Theorem ressbas2 16154

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		df-ss 3730	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2	1	biimpi 206	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = 𝐴)
3		ressbas.b	. . . . 5 ⊢ 𝐵 = (Base‘𝑊)
4		fvex 6364	. . . . 5 ⊢ (Base‘𝑊) ∈ V
5	3, 4	eqeltri 2836	. . . 4 ⊢ 𝐵 ∈ V
6	5	ssex 4955	. . 3 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
7		ressbas.r	. . . 4 ⊢ 𝑅 = (𝑊 ↾s 𝐴)
8	7, 3	ressbas 16153	. . 3 ⊢ (𝐴 ∈ V → (𝐴 ∩ 𝐵) = (Base‘𝑅))
9	6, 8	syl 17	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = (Base‘𝑅))
10	2, 9	eqtr3d 2797	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘𝑅))

Syntax hints:   → wi 4   = wceq 1632   ∈ wcel 2140  Vcvv 3341   ∩ cin 3715   ⊆ wss 3716  ‘cfv 6050  (class class class)co 6815  Basecbs 16080   ↾_s cress 16081

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116  ax-cnex 10205  ax-resscn 10206  ax-1cn 10207  ax-icn 10208  ax-addcl 10209  ax-addrcl 10210  ax-mulcl 10211  ax-mulrcl 10212  ax-i2m1 10217  ax-1ne0 10218  ax-rrecex 10221  ax-cnre 10222

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3343  df-sbc 3578  df-csb 3676  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-pss 3732  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-tp 4327  df-op 4329  df-uni 4590  df-iun 4675  df-br 4806  df-opab 4866  df-mpt 4883  df-tr 4906  df-id 5175  df-eprel 5180  df-po 5188  df-so 5189  df-fr 5226  df-we 5228  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-pred 5842  df-ord 5888  df-on 5889  df-lim 5890  df-suc 5891  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057  df-fv 6058  df-ov 6818  df-oprab 6819  df-mpt2 6820  df-om 7233  df-wrecs 7578  df-recs 7639  df-rdg 7677  df-nn 11234  df-ndx 16083  df-slot 16084  df-base 16086  df-sets 16087  df-ress 16088

This theorem is referenced by:  rescbas  16711  fullresc  16733  resssetc  16964  yoniso  17147  issstrmgm  17474  gsumress  17498  issubmnd  17540  ress0g  17541  submnd0  17542  submbas  17577  resmhm  17581  resgrpplusfrn  17658  subgbas  17820  issubg2  17831  resghm  17898  submod  18205  ringidss  18798  unitgrpbas  18887  isdrng2  18980  drngmcl  18983  drngid2  18986  isdrngd  18995  islss3  19182  lsslss  19184  lsslsp  19238  reslmhm  19275  issubassa  19547  resspsrbas  19638  mplbas  19652  ressmplbas  19679  evlssca  19745  mpfconst  19753  mpfind  19759  ply1bas  19788  ressply1bas  19822  evls1sca  19911  xrs1mnd  20007  xrs10  20008  xrs1cmn  20009  xrge0subm  20010  xrge0cmn  20011  cnmsubglem  20032  nn0srg  20039  rge0srg  20040  zringbas  20047  expghm  20067  cnmsgnbas  20147  psgnghm  20149  rebase  20175  dsmmbase  20302  dsmmval2  20303  lsslindf  20392  lsslinds  20393  islinds3  20396  m2cpmrngiso  20786  ressusp  22291  imasdsf1olem  22400  xrge0gsumle  22858  xrge0tsms  22859  cmsss  23368  minveclem3a  23419  efabl  24517  efsubm  24518  qrngbas  25529  ressplusf  29981  ressnm  29982  ressprs  29986  ressmulgnn  30014  ressmulgnn0  30015  xrge0tsmsd  30116  ress1r  30120  xrge0slmod  30175  prsssdm  30294  ordtrestNEW  30298  ordtrest2NEW  30300  xrge0iifmhm  30316  esumpfinvallem  30467  sitgaddlemb  30741  prdsbnd2  33926  cnpwstotbnd  33928  repwsmet  33965  rrnequiv  33966  lcdvbase  37403  islssfg  38161  lnmlsslnm  38172  pwssplit4  38180  cntzsdrg  38293  deg1mhm  38306  gsumge0cl  41110  sge0tsms  41119  cnfldsrngbas  42298  issubmgm2  42319  submgmbas  42325  resmgmhm  42327  amgmlemALT  43081