Theorem ressbas2 16875

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 3900	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2	1	biimpi 215	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = 𝐴)
3		ressbas.b	. . . . 5 ⊢ 𝐵 = (Base‘𝑊)
4	3	fvexi 6770	. . . 4 ⊢ 𝐵 ∈ V
5	4	ssex 5240	. . 3 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
6		ressbas.r	. . . 4 ⊢ 𝑅 = (𝑊 ↾s 𝐴)
7	6, 3	ressbas 16873	. . 3 ⊢ (𝐴 ∈ V → (𝐴 ∩ 𝐵) = (Base‘𝑅))
8	5, 7	syl 17	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = (Base‘𝑅))
9	2, 8	eqtr3d 2780	1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘𝑅))

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  Vcvv 3422   ∩ cin 3882   ⊆ wss 3883  ‘cfv 6418  (class class class)co 7255  Basecbs 16840   ↾_s cress 16867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-1cn 10860  ax-addcl 10862

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-nn 11904  df-sets 16793  df-slot 16811  df-ndx 16823  df-base 16841  df-ress 16868

This theorem is referenced by:  rescbas  17458  rescbasOLD  17459  fullresc  17482  resssetc  17723  yoniso  17919  issstrmgm  18252  gsumress  18281  issubmnd  18327  ress0g  18328  submnd0  18329  submbas  18368  resmhm  18374  resgrpplusfrn  18508  subgbas  18674  issubg2  18685  resghm  18765  symgbas  18893  submod  19089  cntrcmnd  19358  ringidss  19731  unitgrpbas  19823  isdrng2  19916  drngmcl  19919  drngid2  19922  isdrngd  19931  cntzsdrg  19985  subdrgint  19986  primefld  19988  islss3  20136  lsslss  20138  lsslsp  20192  reslmhm  20229  xrs1mnd  20548  xrs10  20549  xrs1cmn  20550  xrge0subm  20551  xrge0cmn  20552  cnmsubglem  20573  nn0srg  20580  rge0srg  20581  zringbas  20588  expghm  20609  cnmsgnbas  20695  psgnghm  20697  rebase  20723  dsmmbase  20852  dsmmval2  20853  lsslindf  20947  lsslinds  20948  islinds3  20951  resspsrbas  21094  mplbas  21108  ressmplbas  21139  evlssca  21209  mpfconst  21221  mpfind  21227  ply1bas  21276  ressply1bas  21310  evls1sca  21399  m2cpmrngiso  21815  ressusp  23324  imasdsf1olem  23434  xrge0gsumle  23902  xrge0tsms  23903  cmssmscld  24419  cmsss  24420  minveclem3a  24496  efabl  25611  efsubm  25612  qrngbas  26672  ressplusf  31137  ressnm  31138  ressprs  31143  ressmulgnn  31194  ressmulgnn0  31195  xrge0tsmsd  31219  ress1r  31388  xrge0slmod  31450  znfermltl  31464  drgextlsp  31583  lssdimle  31593  lbslsat  31601  dimkerim  31610  fedgmullem1  31612  fedgmullem2  31613  fedgmul  31614  rspecbas  31717  prsssdm  31769  ordtrestNEW  31773  ordtrest2NEW  31775  xrge0iifmhm  31791  esumpfinvallem  31942  sitgaddlemb  32215  prdsbnd2  35880  cnpwstotbnd  35882  repwsmet  35919  rrnequiv  35920  lcdvbase  39534  selvval2lem4  40154  islssfg  40811  lnmlsslnm  40822  pwssplit4  40830  deg1mhm  40948  gsumge0cl  43799  sge0tsms  43808  cnfldsrngbas  45211  issubmgm2  45232  submgmbas  45238  resmgmhm  45240  amgmlemALT  46393