Theorem ressbas2 17208

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 3932	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2	1	biimpi 216	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = 𝐴)
3		ressbas.b	. . . . 5 ⊢ 𝐵 = (Base‘𝑊)
4	3	fvexi 6872	. . . 4 ⊢ 𝐵 ∈ V
5	4	ssex 5276	. . 3 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
6		ressbas.r	. . . 4 ⊢ 𝑅 = (𝑊 ↾s 𝐴)
7	6, 3	ressbas 17206	. . 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 3447   ∩ cin 3913   ⊆ wss 3914  ‘cfv 6511  (class class class)co 7387  Basecbs 17179   ↾_s cress 17200

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 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-1cn 11126  ax-addcl 11128

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 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-nn 12187  df-sets 17134  df-slot 17152  df-ndx 17164  df-base 17180  df-ress 17201

This theorem is referenced by:  rescbas  17791  fullresc  17813  resssetc  18054  yoniso  18246  issstrmgm  18580  gsumress  18609  issubmgm2  18630  submgmbas  18636  resmgmhm  18638  issubmnd  18688  ress0g  18689  submnd0  18690  submbas  18741  resmhm  18747  resgrpplusfrn  18882  ressmulgnn  19008  ressmulgnn0  19009  ressmulgnnd  19010  subgbas  19062  issubg2  19073  resghm  19164  symgbas  19302  finodsubmsubg  19497  submod  19499  cntrcmnd  19772  ringidss  20186  unitgrpbas  20291  isdrng2  20652  drngmclOLD  20660  drngid2  20661  isdrngd  20674  isdrngdOLD  20676  sdrgbas  20703  cntzsdrg  20711  subdrgint  20712  primefld  20714  islss3  20865  lsslss  20867  lsslsp  20921  lsslspOLD  20922  reslmhm  20959  2idlbas  21173  rng2idl1cntr  21215  xrs1mnd  21321  xrs10  21322  xrs1cmn  21323  xrge0subm  21324  xrge0cmn  21325  cnmsubglem  21347  nn0srg  21354  rge0srg  21355  zringbas  21363  expghm  21385  fermltlchr  21439  cnmsgnbas  21487  psgnghm  21489  rebase  21515  dsmmbase  21644  dsmmval2  21645  lsslindf  21739  lsslinds  21740  islinds3  21743  resspsrbas  21883  mplbas  21899  ressmplbas  21935  evlssca  21996  mpfconst  22008  mpfind  22014  ply1bas  22079  ply1basOLD  22080  ressply1bas  22113  evls1sca  22210  evls1fpws  22256  evls1vsca  22260  asclply1subcl  22261  evls1maplmhm  22264  m2cpmrngiso  22645  ressusp  24152  imasdsf1olem  24261  xrge0gsumle  24722  xrge0tsms  24723  cmssmscld  25250  cmsss  25251  minveclem3a  25327  efabl  26459  efsubm  26460  qrngbas  27530  ressplusf  32885  ressnm  32886  ressprs  32890  subgmulgcld  32984  ressmulgnn0d  32985  xrge0tsmsd  33002  ress1r  33185  subrdom  33235  subsdrg  33248  idomsubr  33259  xrge0slmod  33319  znfermltl  33337  ressply1evls1  33534  ressasclcl  33540  resssra  33583  drgextlsp  33589  lssdimle  33603  lbslsat  33612  ply1degltdimlem  33618  ply1degltdim  33619  dimkerim  33623  fedgmullem1  33625  fedgmullem2  33626  fedgmul  33627  dimlssid  33628  lvecendof1f1o  33629  sdrgfldext  33646  fldsdrgfldext  33657  fldsdrgfldext2  33658  fldgenfldext  33663  evls1fldgencl  33665  fldextrspunlsplem  33668  fldextrspunlsp  33669  fldextrspunlem1  33670  fldextrspunfld  33671  fldextrspundgle  33673  fldextrspundgdvdslem  33675  fldextrspundgdvds  33676  0ringirng  33684  algextdeglem3  33709  algextdeglem4  33710  algextdeglem8  33714  rtelextdg2lem  33716  rtelextdg2  33717  constrext2chnlem  33740  2sqr3minply  33770  rspecbas  33855  prsssdm  33907  ordtrestNEW  33911  ordtrest2NEW  33913  xrge0iifmhm  33929  esumpfinvallem  34064  sitgaddlemb  34339  prdsbnd2  37789  cnpwstotbnd  37791  repwsmet  37828  rrnequiv  37829  lcdvbase  41587  primrootsunit1  42085  primrootscoprmpow  42087  primrootscoprbij  42090  aks6d1c6lem4  42161  aks6d1c6isolem2  42163  aks6d1c6lem5  42165  aks5lem7  42188  islssfg  43059  lnmlsslnm  43070  pwssplit4  43078  deg1mhm  43189  gsumge0cl  46369  sge0tsms  46378  cnfldsrngbas  48149  amgmlemALT  49792