Theorem ressbas2 17259

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  Vcvv 3459   ∩ cin 3925   ⊆ wss 3926  ‘cfv 6531  (class class class)co 7405  Basecbs 17228   ↾_s cress 17251

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-cnex 11185  ax-1cn 11187  ax-addcl 11189

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7862  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-nn 12241  df-sets 17183  df-slot 17201  df-ndx 17213  df-base 17229  df-ress 17252

This theorem is referenced by:  rescbas  17842  fullresc  17864  resssetc  18105  yoniso  18297  issstrmgm  18631  gsumress  18660  issubmgm2  18681  submgmbas  18687  resmgmhm  18689  issubmnd  18739  ress0g  18740  submnd0  18741  submbas  18792  resmhm  18798  resgrpplusfrn  18933  ressmulgnn  19059  ressmulgnn0  19060  ressmulgnnd  19061  subgbas  19113  issubg2  19124  resghm  19215  symgbas  19353  finodsubmsubg  19548  submod  19550  cntrcmnd  19823  ringidss  20237  unitgrpbas  20342  isdrng2  20703  drngmclOLD  20711  drngid2  20712  isdrngd  20725  isdrngdOLD  20727  sdrgbas  20754  cntzsdrg  20762  subdrgint  20763  primefld  20765  islss3  20916  lsslss  20918  lsslsp  20972  lsslspOLD  20973  reslmhm  21010  2idlbas  21224  rng2idl1cntr  21266  xrs1mnd  21372  xrs10  21373  xrs1cmn  21374  xrge0subm  21375  xrge0cmn  21376  cnmsubglem  21398  nn0srg  21405  rge0srg  21406  zringbas  21414  expghm  21436  fermltlchr  21490  cnmsgnbas  21538  psgnghm  21540  rebase  21566  dsmmbase  21695  dsmmval2  21696  lsslindf  21790  lsslinds  21791  islinds3  21794  resspsrbas  21934  mplbas  21950  ressmplbas  21986  evlssca  22047  mpfconst  22059  mpfind  22065  ply1bas  22130  ply1basOLD  22131  ressply1bas  22164  evls1sca  22261  evls1fpws  22307  evls1vsca  22311  asclply1subcl  22312  evls1maplmhm  22315  m2cpmrngiso  22696  ressusp  24203  imasdsf1olem  24312  xrge0gsumle  24773  xrge0tsms  24774  cmssmscld  25302  cmsss  25303  minveclem3a  25379  efabl  26511  efsubm  26512  qrngbas  27582  ressplusf  32939  ressnm  32940  ressprs  32944  subgmulgcld  33038  ressmulgnn0d  33039  xrge0tsmsd  33056  ress1r  33229  subrdom  33279  subsdrg  33292  idomsubr  33303  xrge0slmod  33363  znfermltl  33381  ressply1evls1  33578  ressasclcl  33584  resssra  33627  drgextlsp  33633  lssdimle  33647  lbslsat  33656  ply1degltdimlem  33662  ply1degltdim  33663  dimkerim  33667  fedgmullem1  33669  fedgmullem2  33670  fedgmul  33671  dimlssid  33672  lvecendof1f1o  33673  sdrgfldext  33692  fldsdrgfldext  33703  fldsdrgfldext2  33704  fldgenfldext  33709  evls1fldgencl  33711  fldextrspunlsplem  33714  fldextrspunlsp  33715  fldextrspunlem1  33716  fldextrspunfld  33717  fldextrspundgle  33719  fldextrspundgdvdslem  33721  fldextrspundgdvds  33722  0ringirng  33730  algextdeglem3  33753  algextdeglem4  33754  algextdeglem8  33758  rtelextdg2lem  33760  rtelextdg2  33761  constrext2chnlem  33784  2sqr3minply  33814  rspecbas  33896  prsssdm  33948  ordtrestNEW  33952  ordtrest2NEW  33954  xrge0iifmhm  33970  esumpfinvallem  34105  sitgaddlemb  34380  prdsbnd2  37819  cnpwstotbnd  37821  repwsmet  37858  rrnequiv  37859  lcdvbase  41612  primrootsunit1  42110  primrootscoprmpow  42112  primrootscoprbij  42115  aks6d1c6lem4  42186  aks6d1c6isolem2  42188  aks6d1c6lem5  42190  aks5lem7  42213  islssfg  43094  lnmlsslnm  43105  pwssplit4  43113  deg1mhm  43224  gsumge0cl  46400  sge0tsms  46409  cnfldsrngbas  48136  amgmlemALT  49667