Theorem ressbas2 17178

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		df-ss 3964	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2	1	biimpi 215	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = 𝐴)
3		ressbas.b	. . . . 5 ⊢ 𝐵 = (Base‘𝑊)
4	3	fvexi 6902	. . . 4 ⊢ 𝐵 ∈ V
5	4	ssex 5320	. . 3 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
6		ressbas.r	. . . 4 ⊢ 𝑅 = (𝑊 ↾s 𝐴)
7	6, 3	ressbas 17175	. . 3 ⊢ (𝐴 ∈ V → (𝐴 ∩ 𝐵) = (Base‘𝑅))
8	5, 7	syl 17	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = (Base‘𝑅))
9	2, 8	eqtr3d 2774	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘𝑅))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  Vcvv 3474   ∩ cin 3946   ⊆ wss 3947  ‘cfv 6540  (class class class)co 7405  Basecbs 17140   ↾_s cress 17169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-1cn 11164  ax-addcl 11166

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-nn 12209  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170

This theorem is referenced by:  rescbas  17772  rescbasOLD  17773  fullresc  17797  resssetc  18038  yoniso  18234  issstrmgm  18568  gsumress  18597  issubmnd  18648  ress0g  18649  submnd0  18650  submbas  18691  resmhm  18697  resgrpplusfrn  18832  subgbas  19004  issubg2  19015  resghm  19102  symgbas  19232  finodsubmsubg  19429  submod  19431  cntrcmnd  19704  ringidss  20087  unitgrpbas  20188  isdrng2  20321  drngmcl  20324  drngid2  20328  isdrngd  20340  isdrngdOLD  20342  sdrgbas  20402  cntzsdrg  20410  subdrgint  20411  primefld  20413  islss3  20562  lsslss  20564  lsslsp  20618  reslmhm  20655  2idlbas  20861  xrs1mnd  20975  xrs10  20976  xrs1cmn  20977  xrge0subm  20978  xrge0cmn  20979  cnmsubglem  21000  nn0srg  21007  rge0srg  21008  zringbas  21015  expghm  21036  cnmsgnbas  21122  psgnghm  21124  rebase  21150  dsmmbase  21281  dsmmval2  21282  lsslindf  21376  lsslinds  21377  islinds3  21380  resspsrbas  21526  mplbas  21540  ressmplbas  21574  evlssca  21643  mpfconst  21655  mpfind  21661  ply1bas  21710  ressply1bas  21742  evls1sca  21833  m2cpmrngiso  22251  ressusp  23760  imasdsf1olem  23870  xrge0gsumle  24340  xrge0tsms  24341  cmssmscld  24858  cmsss  24859  minveclem3a  24935  efabl  26050  efsubm  26051  qrngbas  27111  ressplusf  32114  ressnm  32115  ressprs  32120  ressmulgnn  32171  ressmulgnn0  32172  xrge0tsmsd  32196  ress1r  32371  xrge0slmod  32451  fermltlchr  32466  znfermltl  32467  evls1fpws  32634  evls1vsca  32638  asclply1subcl  32648  drgextlsp  32669  lssdimle  32680  lbslsat  32689  ply1degltdimlem  32695  ply1degltdim  32696  dimkerim  32700  fedgmullem1  32702  fedgmullem2  32703  fedgmul  32704  0ringirng  32741  evls1maplmhm  32748  algextdeglem1  32760  rspecbas  32833  prsssdm  32885  ordtrestNEW  32889  ordtrest2NEW  32891  xrge0iifmhm  32907  esumpfinvallem  33060  sitgaddlemb  33335  prdsbnd2  36651  cnpwstotbnd  36653  repwsmet  36690  rrnequiv  36691  lcdvbase  40452  islssfg  41797  lnmlsslnm  41808  pwssplit4  41816  deg1mhm  41934  gsumge0cl  45073  sge0tsms  45082  cnfldsrngbas  46525  issubmgm2  46546  submgmbas  46552  resmgmhm  46554  rng2idl1cntr  46770  amgmlemALT  47803