Theorem ressbas2 17323

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 3926	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2	1	biimpi 219	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = 𝐴)
3		ressbas.b	. . . . 5 ⊢ 𝐵 = (Base‘𝑊)
4	3	fvexi 6902	. . . 4 ⊢ 𝐵 ∈ V
5	4	ssex 5296	. . 3 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
6		ressbas.r	. . . 4 ⊢ 𝑅 = (𝑊 ↾s 𝐴)
7	6, 3	ressbas 17321	. . 3 ⊢ (𝐴 ∈ V → (𝐴 ∩ 𝐵) = (Base‘𝑅))
8	5, 7	syl 18	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = (Base‘𝑅))
9	2, 8	eqtr3d 2803	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘𝑅))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  Vcvv 3458   ∩ cin 3907   ⊆ wss 3908  ‘cfv 6543  (class class class)co 7423  Basecbs 17294   ↾_s cress 17315

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-cnex 11174  ax-1cn 11176  ax-addcl 11178

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7872  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-nn 12252  df-sets 17249  df-slot 17267  df-ndx 17279  df-base 17295  df-ress 17316

This theorem is used by:  rescbas  17911  fullresc  17933  resssetc  18174  yoniso  18366  issstrmgm  18736  gsumress  18765  issubmgm2  18786  submgmbas  18792  resmgmhm  18794  issubmnd  18844  ress0g  18845  submnd0  18846  submbas  18898  resmhm  18904  resgrpplusfrn  19042  ressmulgnn  19167  ressmulgnn0  19168  ressmulgnnd  19169  subgbas  19221  issubg2  19233  resghm  19327  symgbas  19467  finodsubmsubg  19662  submod  19664  cntrcmnd  19937  ringidss  20386  unitgrpbas  20490  isdrng2  20873  isdrng3lem0  20880  drngid2  20886  isdrngd  20898  isdrngdOLD  20900  sdrgbas  20927  cntzsdrg  20935  subdrgint  20936  primefld  20938  islss3  21110  lsslss  21112  lsslsp  21166  reslmhm  21203  2idlbas  21432  rng2idl1cntr  21475  cnmsubglem  21610  nn0srg  21617  rge0srg  21618  xrs1mnd  21620  xrs10  21621  xrs1cmn  21622  xrge0subm  21623  xrge0cmn  21624  zringbas  21633  expghm  21655  fermltlchr  21709  cnmsgnbas  21758  psgnghm  21760  rebase  21786  dsmmbase  21915  dsmmval2  21916  lsslindf  22010  lsslinds  22011  islinds3  22014  resspsrbas  22153  mplbas  22169  ressmplbas  22208  evlssca  22275  mpfconst  22290  mpfind  22296  ply1bas  22385  ressply1bas  22418  evls1sca  22513  evls1fpws  22559  evls1vsca  22563  asclply1subcl  22564  evls1maplmhm  22567  m2cpmrngiso  22945  ressusp  24451  imasdsf1olem  24560  xrge0gsumle  25021  xrge0tsms  25022  cmssmscld  25539  cmsss  25540  minveclem3a  25616  efabl  26745  efsubm  26746  qrngbas  27813  ressplusf  33307  ressnm  33308  ressprs  33310  subgmulgcld  33387  ressmulgnn0d  33388  xrge0tsmsd  33417  ress1r  33576  subrdom  33629  subsdrg  33643  idomsubr  33654  xrge0slmod  33692  znfermltl  33705  ressply1evls1  33879  ressasclcl  33885  resssra  34001  drgextlsp  34008  lssdimle  34022  lbslsat  34030  ply1degltdimlem  34036  ply1degltdim  34037  dimkerim  34041  fedgmullem1  34043  fedgmullem2  34044  fedgmul  34045  dimlssid  34046  lvecendof1f1o  34047  sdrgfldext  34064  fldsdrgfldext  34075  fldsdrgfldext2  34076  fldgenfldext  34082  evls1fldgencl  34084  fldextrspunlsplem  34087  fldextrspunlsp  34088  fldextrspunlem1  34089  fldextrspunfld  34090  fldextrspundgle  34092  fldextrspundgdvdslem  34094  fldextrspundgdvds  34095  0ringirng  34103  extdgfialglem1  34106  extdgfialglem2  34107  algextdeglem3  34133  algextdeglem4  34134  algextdeglem8  34138  rtelextdg2lem  34140  rtelextdg2  34141  constrext2chnlem  34164  2sqr3minply  34194  rspecbas  34279  prsssdm  34331  ordtrestNEW  34335  ordtrest2NEW  34337  xrge0iifmhm  34353  esumpfinvallem  34488  sitgaddlemb  34762  prdsbnd2  38479  cnpwstotbnd  38481  repwsmet  38518  rrnequiv  38519  lcdvbase  42400  primrootsunit1  42897  primrootscoprmpow  42899  primrootscoprbij  42902  aks6d1c6lem4  42973  aks6d1c6isolem2  42975  aks6d1c6lem5  42977  aks5lem7  43000  islssfg  43830  lnmlsslnm  43841  pwssplit4  43849  deg1mhm  43960  gsumge0cl  47118  sge0tsms  47127  cnfldsrngbas  48959  amgmlemALT  50684