Theorem ressbas2 17165

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  Vcvv 3440   ∩ cin 3900   ⊆ wss 3901  ‘cfv 6492  (class class class)co 7358  Basecbs 17136   ↾_s cress 17157

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-1cn 11084  ax-addcl 11086

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-nn 12146  df-sets 17091  df-slot 17109  df-ndx 17121  df-base 17137  df-ress 17158

This theorem is referenced by:  rescbas  17753  fullresc  17775  resssetc  18016  yoniso  18208  issstrmgm  18578  gsumress  18607  issubmgm2  18628  submgmbas  18634  resmgmhm  18636  issubmnd  18686  ress0g  18687  submnd0  18688  submbas  18739  resmhm  18745  resgrpplusfrn  18880  ressmulgnn  19006  ressmulgnn0  19007  ressmulgnnd  19008  subgbas  19060  issubg2  19071  resghm  19161  symgbas  19301  finodsubmsubg  19496  submod  19498  cntrcmnd  19771  ringidss  20212  unitgrpbas  20318  isdrng2  20676  drngmclOLD  20684  drngid2  20685  isdrngd  20698  isdrngdOLD  20700  sdrgbas  20727  cntzsdrg  20735  subdrgint  20736  primefld  20738  islss3  20910  lsslss  20912  lsslsp  20966  lsslspOLD  20967  reslmhm  21004  2idlbas  21218  rng2idl1cntr  21260  cnmsubglem  21385  nn0srg  21392  rge0srg  21393  xrs1mnd  21395  xrs10  21396  xrs1cmn  21397  xrge0subm  21398  xrge0cmn  21399  zringbas  21408  expghm  21430  fermltlchr  21484  cnmsgnbas  21533  psgnghm  21535  rebase  21561  dsmmbase  21690  dsmmval2  21691  lsslindf  21785  lsslinds  21786  islinds3  21789  resspsrbas  21929  mplbas  21945  ressmplbas  21983  evlssca  22049  mpfconst  22064  mpfind  22070  ply1bas  22135  ply1basOLD  22136  ressply1bas  22169  evls1sca  22267  evls1fpws  22313  evls1vsca  22317  asclply1subcl  22318  evls1maplmhm  22321  m2cpmrngiso  22702  ressusp  24208  imasdsf1olem  24317  xrge0gsumle  24778  xrge0tsms  24779  cmssmscld  25306  cmsss  25307  minveclem3a  25383  efabl  26515  efsubm  26516  qrngbas  27586  ressplusf  33045  ressnm  33046  ressprs  33048  subgmulgcld  33126  ressmulgnn0d  33127  xrge0tsmsd  33155  ress1r  33315  subrdom  33367  subsdrg  33380  idomsubr  33391  xrge0slmod  33429  znfermltl  33447  ressply1evls1  33646  ressasclcl  33652  resssra  33743  drgextlsp  33750  lssdimle  33764  lbslsat  33773  ply1degltdimlem  33779  ply1degltdim  33780  dimkerim  33784  fedgmullem1  33786  fedgmullem2  33787  fedgmul  33788  dimlssid  33789  lvecendof1f1o  33790  sdrgfldext  33807  fldsdrgfldext  33818  fldsdrgfldext2  33819  fldgenfldext  33825  evls1fldgencl  33827  fldextrspunlsplem  33830  fldextrspunlsp  33831  fldextrspunlem1  33832  fldextrspunfld  33833  fldextrspundgle  33835  fldextrspundgdvdslem  33837  fldextrspundgdvds  33838  0ringirng  33846  extdgfialglem1  33849  extdgfialglem2  33850  algextdeglem3  33876  algextdeglem4  33877  algextdeglem8  33881  rtelextdg2lem  33883  rtelextdg2  33884  constrext2chnlem  33907  2sqr3minply  33937  rspecbas  34022  prsssdm  34074  ordtrestNEW  34078  ordtrest2NEW  34080  xrge0iifmhm  34096  esumpfinvallem  34231  sitgaddlemb  34505  prdsbnd2  37996  cnpwstotbnd  37998  repwsmet  38035  rrnequiv  38036  lcdvbase  41853  primrootsunit1  42351  primrootscoprmpow  42353  primrootscoprbij  42356  aks6d1c6lem4  42427  aks6d1c6isolem2  42429  aks6d1c6lem5  42431  aks5lem7  42454  islssfg  43312  lnmlsslnm  43323  pwssplit4  43331  deg1mhm  43442  gsumge0cl  46615  sge0tsms  46624  cnfldsrngbas  48407  amgmlemALT  50048