Theorem ressbas2 17144

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 3915	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2	1	biimpi 216	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = 𝐴)
3		ressbas.b	. . . . 5 ⊢ 𝐵 = (Base‘𝑊)
4	3	fvexi 6831	. . . 4 ⊢ 𝐵 ∈ V
5	4	ssex 5254	. . 3 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
6		ressbas.r	. . . 4 ⊢ 𝑅 = (𝑊 ↾s 𝐴)
7	6, 3	ressbas 17142	. . 3 ⊢ (𝐴 ∈ V → (𝐴 ∩ 𝐵) = (Base‘𝑅))
8	5, 7	syl 17	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = (Base‘𝑅))
9	2, 8	eqtr3d 2768	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘𝑅))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  Vcvv 3436   ∩ cin 3896   ⊆ wss 3897  ‘cfv 6476  (class class class)co 7341  Basecbs 17115   ↾_s cress 17136

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pow 5298  ax-pr 5365  ax-un 7663  ax-cnex 11057  ax-1cn 11059  ax-addcl 11061

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5506  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5564  df-we 5566  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-pred 6243  df-ord 6304  df-on 6305  df-lim 6306  df-suc 6307  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-ov 7344  df-oprab 7345  df-mpo 7346  df-om 7792  df-2nd 7917  df-frecs 8206  df-wrecs 8237  df-recs 8286  df-rdg 8324  df-nn 12121  df-sets 17070  df-slot 17088  df-ndx 17100  df-base 17116  df-ress 17137

This theorem is referenced by:  rescbas  17731  fullresc  17753  resssetc  17994  yoniso  18186  issstrmgm  18556  gsumress  18585  issubmgm2  18606  submgmbas  18612  resmgmhm  18614  issubmnd  18664  ress0g  18665  submnd0  18666  submbas  18717  resmhm  18723  resgrpplusfrn  18858  ressmulgnn  18984  ressmulgnn0  18985  ressmulgnnd  18986  subgbas  19038  issubg2  19049  resghm  19139  symgbas  19279  finodsubmsubg  19474  submod  19476  cntrcmnd  19749  ringidss  20190  unitgrpbas  20295  isdrng2  20653  drngmclOLD  20661  drngid2  20662  isdrngd  20675  isdrngdOLD  20677  sdrgbas  20704  cntzsdrg  20712  subdrgint  20713  primefld  20715  islss3  20887  lsslss  20889  lsslsp  20943  lsslspOLD  20944  reslmhm  20981  2idlbas  21195  rng2idl1cntr  21237  cnmsubglem  21362  nn0srg  21369  rge0srg  21370  xrs1mnd  21372  xrs10  21373  xrs1cmn  21374  xrge0subm  21375  xrge0cmn  21376  zringbas  21385  expghm  21407  fermltlchr  21461  cnmsgnbas  21510  psgnghm  21512  rebase  21538  dsmmbase  21667  dsmmval2  21668  lsslindf  21762  lsslinds  21763  islinds3  21766  resspsrbas  21906  mplbas  21922  ressmplbas  21958  evlssca  22019  mpfconst  22031  mpfind  22037  ply1bas  22102  ply1basOLD  22103  ressply1bas  22136  evls1sca  22233  evls1fpws  22279  evls1vsca  22283  asclply1subcl  22284  evls1maplmhm  22287  m2cpmrngiso  22668  ressusp  24174  imasdsf1olem  24283  xrge0gsumle  24744  xrge0tsms  24745  cmssmscld  25272  cmsss  25273  minveclem3a  25349  efabl  26481  efsubm  26482  qrngbas  27552  ressplusf  32936  ressnm  32937  ressprs  32939  subgmulgcld  33016  ressmulgnn0d  33017  xrge0tsmsd  33034  ress1r  33193  subrdom  33243  subsdrg  33256  idomsubr  33267  xrge0slmod  33305  znfermltl  33323  ressply1evls1  33520  ressasclcl  33526  resssra  33591  drgextlsp  33598  lssdimle  33612  lbslsat  33621  ply1degltdimlem  33627  ply1degltdim  33628  dimkerim  33632  fedgmullem1  33634  fedgmullem2  33635  fedgmul  33636  dimlssid  33637  lvecendof1f1o  33638  sdrgfldext  33655  fldsdrgfldext  33666  fldsdrgfldext2  33667  fldgenfldext  33673  evls1fldgencl  33675  fldextrspunlsplem  33678  fldextrspunlsp  33679  fldextrspunlem1  33680  fldextrspunfld  33681  fldextrspundgle  33683  fldextrspundgdvdslem  33685  fldextrspundgdvds  33686  0ringirng  33694  extdgfialglem1  33697  extdgfialglem2  33698  algextdeglem3  33724  algextdeglem4  33725  algextdeglem8  33729  rtelextdg2lem  33731  rtelextdg2  33732  constrext2chnlem  33755  2sqr3minply  33785  rspecbas  33870  prsssdm  33922  ordtrestNEW  33926  ordtrest2NEW  33928  xrge0iifmhm  33944  esumpfinvallem  34079  sitgaddlemb  34353  prdsbnd2  37835  cnpwstotbnd  37837  repwsmet  37874  rrnequiv  37875  lcdvbase  41632  primrootsunit1  42130  primrootscoprmpow  42132  primrootscoprbij  42135  aks6d1c6lem4  42206  aks6d1c6isolem2  42208  aks6d1c6lem5  42210  aks5lem7  42233  islssfg  43103  lnmlsslnm  43114  pwssplit4  43122  deg1mhm  43233  gsumge0cl  46409  sge0tsms  46418  cnfldsrngbas  48192  amgmlemALT  49835