Theorem ressbas2 17187

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2105  Vcvv 3473   ∩ cin 3947   ⊆ wss 3948  ‘cfv 6543  (class class class)co 7412  Basecbs 17149   ↾_s cress 17178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7728  ax-cnex 11169  ax-1cn 11171  ax-addcl 11173

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7859  df-2nd 7979  df-frecs 8269  df-wrecs 8300  df-recs 8374  df-rdg 8413  df-nn 12218  df-sets 17102  df-slot 17120  df-ndx 17132  df-base 17150  df-ress 17179

This theorem is referenced by:  rescbas  17781  rescbasOLD  17782  fullresc  17806  resssetc  18047  yoniso  18243  issstrmgm  18579  gsumress  18608  issubmgm2  18629  submgmbas  18635  resmgmhm  18637  issubmnd  18687  ress0g  18688  submnd0  18689  submbas  18732  resmhm  18738  resgrpplusfrn  18873  subgbas  19047  issubg2  19058  resghm  19147  symgbas  19280  finodsubmsubg  19477  submod  19479  cntrcmnd  19752  ringidss  20166  unitgrpbas  20274  isdrng2  20515  drngmcl  20518  drngid2  20522  isdrngd  20534  isdrngdOLD  20536  sdrgbas  20554  cntzsdrg  20562  subdrgint  20563  primefld  20565  islss3  20715  lsslss  20717  lsslsp  20771  reslmhm  20808  2idlbas  21019  rng2idl1cntr  21065  xrs1mnd  21184  xrs10  21185  xrs1cmn  21186  xrge0subm  21187  xrge0cmn  21188  cnmsubglem  21209  nn0srg  21216  rge0srg  21217  zringbas  21225  expghm  21247  cnmsgnbas  21351  psgnghm  21353  rebase  21379  dsmmbase  21510  dsmmval2  21511  lsslindf  21605  lsslinds  21606  islinds3  21609  resspsrbas  21755  mplbas  21769  ressmplbas  21803  evlssca  21872  mpfconst  21884  mpfind  21890  ply1bas  21939  ressply1bas  21972  evls1sca  22063  m2cpmrngiso  22481  ressusp  23990  imasdsf1olem  24100  xrge0gsumle  24570  xrge0tsms  24571  cmssmscld  25099  cmsss  25100  minveclem3a  25176  efabl  26296  efsubm  26297  qrngbas  27359  ressplusf  32395  ressnm  32396  ressprs  32401  ressmulgnn  32452  ressmulgnn0  32453  xrge0tsmsd  32480  ress1r  32654  xrge0slmod  32734  fermltlchr  32753  znfermltl  32754  evls1fpws  32921  evls1vsca  32925  asclply1subcl  32935  resssra  32963  drgextlsp  32969  lssdimle  32981  lbslsat  32990  ply1degltdimlem  32996  ply1degltdim  32997  dimkerim  33001  fedgmullem1  33003  fedgmullem2  33004  fedgmul  33005  evls1fldgencl  33034  0ringirng  33043  evls1maplmhm  33050  algextdeglem3  33065  algextdeglem4  33066  algextdeglem8  33070  rspecbas  33144  prsssdm  33196  ordtrestNEW  33200  ordtrest2NEW  33202  xrge0iifmhm  33218  esumpfinvallem  33371  sitgaddlemb  33646  prdsbnd2  36967  cnpwstotbnd  36969  repwsmet  37006  rrnequiv  37007  lcdvbase  40768  islssfg  42115  lnmlsslnm  42126  pwssplit4  42134  deg1mhm  42252  gsumge0cl  45386  sge0tsms  45395  cnfldsrngbas  46838  amgmlemALT  47938