Theorem ressbas2 17149

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 3921	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2	1	biimpi 216	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = 𝐴)
3		ressbas.b	. . . . 5 ⊢ 𝐵 = (Base‘𝑊)
4	3	fvexi 6836	. . . 4 ⊢ 𝐵 ∈ V
5	4	ssex 5260	. . 3 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
6		ressbas.r	. . . 4 ⊢ 𝑅 = (𝑊 ↾s 𝐴)
7	6, 3	ressbas 17147	. . 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 3436   ∩ cin 3902   ⊆ wss 3903  ‘cfv 6482  (class class class)co 7349  Basecbs 17120   ↾_s cress 17141

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 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-1cn 11067  ax-addcl 11069

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 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-nn 12129  df-sets 17075  df-slot 17093  df-ndx 17105  df-base 17121  df-ress 17142

This theorem is referenced by:  rescbas  17736  fullresc  17758  resssetc  17999  yoniso  18191  issstrmgm  18527  gsumress  18556  issubmgm2  18577  submgmbas  18583  resmgmhm  18585  issubmnd  18635  ress0g  18636  submnd0  18637  submbas  18688  resmhm  18694  resgrpplusfrn  18829  ressmulgnn  18955  ressmulgnn0  18956  ressmulgnnd  18957  subgbas  19009  issubg2  19020  resghm  19111  symgbas  19251  finodsubmsubg  19446  submod  19448  cntrcmnd  19721  ringidss  20162  unitgrpbas  20267  isdrng2  20628  drngmclOLD  20636  drngid2  20637  isdrngd  20650  isdrngdOLD  20652  sdrgbas  20679  cntzsdrg  20687  subdrgint  20688  primefld  20690  islss3  20862  lsslss  20864  lsslsp  20918  lsslspOLD  20919  reslmhm  20956  2idlbas  21170  rng2idl1cntr  21212  cnmsubglem  21337  nn0srg  21344  rge0srg  21345  xrs1mnd  21347  xrs10  21348  xrs1cmn  21349  xrge0subm  21350  xrge0cmn  21351  zringbas  21360  expghm  21382  fermltlchr  21436  cnmsgnbas  21485  psgnghm  21487  rebase  21513  dsmmbase  21642  dsmmval2  21643  lsslindf  21737  lsslinds  21738  islinds3  21741  resspsrbas  21881  mplbas  21897  ressmplbas  21933  evlssca  21994  mpfconst  22006  mpfind  22012  ply1bas  22077  ply1basOLD  22078  ressply1bas  22111  evls1sca  22208  evls1fpws  22254  evls1vsca  22258  asclply1subcl  22259  evls1maplmhm  22262  m2cpmrngiso  22643  ressusp  24150  imasdsf1olem  24259  xrge0gsumle  24720  xrge0tsms  24721  cmssmscld  25248  cmsss  25249  minveclem3a  25325  efabl  26457  efsubm  26458  qrngbas  27528  ressplusf  32905  ressnm  32906  ressprs  32908  subgmulgcld  32997  ressmulgnn0d  32998  xrge0tsmsd  33015  ress1r  33174  subrdom  33224  subsdrg  33237  idomsubr  33248  xrge0slmod  33285  znfermltl  33303  ressply1evls1  33500  ressasclcl  33506  resssra  33553  drgextlsp  33560  lssdimle  33574  lbslsat  33583  ply1degltdimlem  33589  ply1degltdim  33590  dimkerim  33594  fedgmullem1  33596  fedgmullem2  33597  fedgmul  33598  dimlssid  33599  lvecendof1f1o  33600  sdrgfldext  33617  fldsdrgfldext  33628  fldsdrgfldext2  33629  fldgenfldext  33635  evls1fldgencl  33637  fldextrspunlsplem  33640  fldextrspunlsp  33641  fldextrspunlem1  33642  fldextrspunfld  33643  fldextrspundgle  33645  fldextrspundgdvdslem  33647  fldextrspundgdvds  33648  0ringirng  33656  extdgfialglem1  33659  extdgfialglem2  33660  algextdeglem3  33686  algextdeglem4  33687  algextdeglem8  33691  rtelextdg2lem  33693  rtelextdg2  33694  constrext2chnlem  33717  2sqr3minply  33747  rspecbas  33832  prsssdm  33884  ordtrestNEW  33888  ordtrest2NEW  33890  xrge0iifmhm  33906  esumpfinvallem  34041  sitgaddlemb  34316  prdsbnd2  37775  cnpwstotbnd  37777  repwsmet  37814  rrnequiv  37815  lcdvbase  41572  primrootsunit1  42070  primrootscoprmpow  42072  primrootscoprbij  42075  aks6d1c6lem4  42146  aks6d1c6isolem2  42148  aks6d1c6lem5  42150  aks5lem7  42173  islssfg  43043  lnmlsslnm  43054  pwssplit4  43062  deg1mhm  43173  gsumge0cl  46352  sge0tsms  46361  cnfldsrngbas  48145  amgmlemALT  49788