Theorem ressbas2 17184

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3444   ∩ cin 3910   ⊆ wss 3911  ‘cfv 6499  (class class class)co 7369  Basecbs 17155   ↾_s cress 17176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-1cn 11102  ax-addcl 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-oprab 7373  df-mpo 7374  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-nn 12163  df-sets 17110  df-slot 17128  df-ndx 17140  df-base 17156  df-ress 17177

This theorem is referenced by:  rescbas  17767  fullresc  17789  resssetc  18030  yoniso  18222  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  19140  symgbas  19278  finodsubmsubg  19473  submod  19475  cntrcmnd  19748  ringidss  20162  unitgrpbas  20267  isdrng2  20628  drngmclOLD  20636  drngid2  20637  isdrngd  20650  isdrngdOLD  20652  sdrgbas  20679  cntzsdrg  20687  subdrgint  20688  primefld  20690  islss3  20841  lsslss  20843  lsslsp  20897  lsslspOLD  20898  reslmhm  20935  2idlbas  21149  rng2idl1cntr  21191  xrs1mnd  21297  xrs10  21298  xrs1cmn  21299  xrge0subm  21300  xrge0cmn  21301  cnmsubglem  21323  nn0srg  21330  rge0srg  21331  zringbas  21339  expghm  21361  fermltlchr  21415  cnmsgnbas  21463  psgnghm  21465  rebase  21491  dsmmbase  21620  dsmmval2  21621  lsslindf  21715  lsslinds  21716  islinds3  21719  resspsrbas  21859  mplbas  21875  ressmplbas  21911  evlssca  21972  mpfconst  21984  mpfind  21990  ply1bas  22055  ply1basOLD  22056  ressply1bas  22089  evls1sca  22186  evls1fpws  22232  evls1vsca  22236  asclply1subcl  22237  evls1maplmhm  22240  m2cpmrngiso  22621  ressusp  24128  imasdsf1olem  24237  xrge0gsumle  24698  xrge0tsms  24699  cmssmscld  25226  cmsss  25227  minveclem3a  25303  efabl  26435  efsubm  26436  qrngbas  27506  ressplusf  32858  ressnm  32859  ressprs  32863  subgmulgcld  32957  ressmulgnn0d  32958  xrge0tsmsd  32975  ress1r  33158  subrdom  33208  subsdrg  33221  idomsubr  33232  xrge0slmod  33292  znfermltl  33310  ressply1evls1  33507  ressasclcl  33513  resssra  33556  drgextlsp  33562  lssdimle  33576  lbslsat  33585  ply1degltdimlem  33591  ply1degltdim  33592  dimkerim  33596  fedgmullem1  33598  fedgmullem2  33599  fedgmul  33600  dimlssid  33601  lvecendof1f1o  33602  sdrgfldext  33619  fldsdrgfldext  33630  fldsdrgfldext2  33631  fldgenfldext  33636  evls1fldgencl  33638  fldextrspunlsplem  33641  fldextrspunlsp  33642  fldextrspunlem1  33643  fldextrspunfld  33644  fldextrspundgle  33646  fldextrspundgdvdslem  33648  fldextrspundgdvds  33649  0ringirng  33657  algextdeglem3  33682  algextdeglem4  33683  algextdeglem8  33687  rtelextdg2lem  33689  rtelextdg2  33690  constrext2chnlem  33713  2sqr3minply  33743  rspecbas  33828  prsssdm  33880  ordtrestNEW  33884  ordtrest2NEW  33886  xrge0iifmhm  33902  esumpfinvallem  34037  sitgaddlemb  34312  prdsbnd2  37762  cnpwstotbnd  37764  repwsmet  37801  rrnequiv  37802  lcdvbase  41560  primrootsunit1  42058  primrootscoprmpow  42060  primrootscoprbij  42063  aks6d1c6lem4  42134  aks6d1c6isolem2  42136  aks6d1c6lem5  42138  aks5lem7  42161  islssfg  43032  lnmlsslnm  43043  pwssplit4  43051  deg1mhm  43162  gsumge0cl  46342  sge0tsms  46351  cnfldsrngbas  48122  amgmlemALT  49765