Theorem ressbas2 17047

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 3919	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2	1	biimpi 215	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = 𝐴)
3		ressbas.b	. . . . 5 ⊢ 𝐵 = (Base‘𝑊)
4	3	fvexi 6844	. . . 4 ⊢ 𝐵 ∈ V
5	4	ssex 5270	. . 3 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
6		ressbas.r	. . . 4 ⊢ 𝑅 = (𝑊 ↾s 𝐴)
7	6, 3	ressbas 17045	. . 3 ⊢ (𝐴 ∈ V → (𝐴 ∩ 𝐵) = (Base‘𝑅))
8	5, 7	syl 17	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = (Base‘𝑅))
9	2, 8	eqtr3d 2779	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘𝑅))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  Vcvv 3442   ∩ cin 3901   ⊆ wss 3902  ‘cfv 6484  (class class class)co 7342  Basecbs 17010   ↾_s cress 17039

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5248  ax-nul 5255  ax-pow 5313  ax-pr 5377  ax-un 7655  ax-cnex 11033  ax-1cn 11035  ax-addcl 11037

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3351  df-rab 3405  df-v 3444  df-sbc 3732  df-csb 3848  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3921  df-nul 4275  df-if 4479  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4858  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5181  df-tr 5215  df-id 5523  df-eprel 5529  df-po 5537  df-so 5538  df-fr 5580  df-we 5582  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6243  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6436  df-fun 6486  df-fn 6487  df-f 6488  df-f1 6489  df-fo 6490  df-f1o 6491  df-fv 6492  df-ov 7345  df-oprab 7346  df-mpo 7347  df-om 7786  df-2nd 7905  df-frecs 8172  df-wrecs 8203  df-recs 8277  df-rdg 8316  df-nn 12080  df-sets 16963  df-slot 16981  df-ndx 16993  df-base 17011  df-ress 17040

This theorem is referenced by:  rescbas  17639  rescbasOLD  17640  fullresc  17664  resssetc  17905  yoniso  18101  issstrmgm  18435  gsumress  18464  issubmnd  18510  ress0g  18511  submnd0  18512  submbas  18551  resmhm  18557  resgrpplusfrn  18690  subgbas  18856  issubg2  18867  resghm  18947  symgbas  19075  submod  19271  cntrcmnd  19539  ringidss  19911  unitgrpbas  20003  isdrng2  20106  drngmcl  20109  drngid2  20112  isdrngd  20121  cntzsdrg  20176  subdrgint  20177  primefld  20179  islss3  20327  lsslss  20329  lsslsp  20383  reslmhm  20420  xrs1mnd  20742  xrs10  20743  xrs1cmn  20744  xrge0subm  20745  xrge0cmn  20746  cnmsubglem  20767  nn0srg  20774  rge0srg  20775  zringbas  20782  expghm  20803  cnmsgnbas  20889  psgnghm  20891  rebase  20917  dsmmbase  21048  dsmmval2  21049  lsslindf  21143  lsslinds  21144  islinds3  21147  resspsrbas  21290  mplbas  21304  ressmplbas  21335  evlssca  21405  mpfconst  21417  mpfind  21423  ply1bas  21472  ressply1bas  21506  evls1sca  21595  m2cpmrngiso  22013  ressusp  23522  imasdsf1olem  23632  xrge0gsumle  24102  xrge0tsms  24103  cmssmscld  24620  cmsss  24621  minveclem3a  24697  efabl  25812  efsubm  25813  qrngbas  26873  ressplusf  31520  ressnm  31521  ressprs  31526  ressmulgnn  31577  ressmulgnn0  31578  xrge0tsmsd  31602  ress1r  31771  xrge0slmod  31842  fermltlchr  31856  znfermltl  31857  drgextlsp  31977  lssdimle  31987  lbslsat  31995  dimkerim  32004  fedgmullem1  32006  fedgmullem2  32007  fedgmul  32008  rspecbas  32111  prsssdm  32163  ordtrestNEW  32167  ordtrest2NEW  32169  xrge0iifmhm  32185  esumpfinvallem  32338  sitgaddlemb  32613  prdsbnd2  36107  cnpwstotbnd  36109  repwsmet  36146  rrnequiv  36147  lcdvbase  39910  selvval2lem4  40531  islssfg  41207  lnmlsslnm  41218  pwssplit4  41226  deg1mhm  41344  gsumge0cl  44296  sge0tsms  44305  cnfldsrngbas  45739  issubmgm2  45760  submgmbas  45766  resmgmhm  45768  amgmlemALT  46923