Theorem ressbas2 17177

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 3921	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2	1	biimpi 216	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = 𝐴)
3		ressbas.b	. . . . 5 ⊢ 𝐵 = (Base‘𝑊)
4	3	fvexi 6856	. . . 4 ⊢ 𝐵 ∈ V
5	4	ssex 5268	. . 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 1542   ∈ wcel 2114  Vcvv 3442   ∩ cin 3902   ⊆ wss 3903  ‘cfv 6500  (class class class)co 7368  Basecbs 17148   ↾_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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-1cn 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-nn 12158  df-sets 17103  df-slot 17121  df-ndx 17133  df-base 17149  df-ress 17170

This theorem is referenced by:  rescbas  17765  fullresc  17787  resssetc  18028  yoniso  18220  issstrmgm  18590  gsumress  18619  issubmgm2  18640  submgmbas  18646  resmgmhm  18648  issubmnd  18698  ress0g  18699  submnd0  18700  submbas  18751  resmhm  18757  resgrpplusfrn  18892  ressmulgnn  19018  ressmulgnn0  19019  ressmulgnnd  19020  subgbas  19072  issubg2  19083  resghm  19173  symgbas  19313  finodsubmsubg  19508  submod  19510  cntrcmnd  19783  ringidss  20224  unitgrpbas  20330  isdrng2  20688  drngmclOLD  20696  drngid2  20697  isdrngd  20710  isdrngdOLD  20712  sdrgbas  20739  cntzsdrg  20747  subdrgint  20748  primefld  20750  islss3  20922  lsslss  20924  lsslsp  20978  lsslspOLD  20979  reslmhm  21016  2idlbas  21230  rng2idl1cntr  21272  cnmsubglem  21397  nn0srg  21404  rge0srg  21405  xrs1mnd  21407  xrs10  21408  xrs1cmn  21409  xrge0subm  21410  xrge0cmn  21411  zringbas  21420  expghm  21442  fermltlchr  21496  cnmsgnbas  21545  psgnghm  21547  rebase  21573  dsmmbase  21702  dsmmval2  21703  lsslindf  21797  lsslinds  21798  islinds3  21801  resspsrbas  21941  mplbas  21957  ressmplbas  21995  evlssca  22061  mpfconst  22076  mpfind  22082  ply1bas  22147  ply1basOLD  22148  ressply1bas  22181  evls1sca  22279  evls1fpws  22325  evls1vsca  22329  asclply1subcl  22330  evls1maplmhm  22333  m2cpmrngiso  22714  ressusp  24220  imasdsf1olem  24329  xrge0gsumle  24790  xrge0tsms  24791  cmssmscld  25318  cmsss  25319  minveclem3a  25395  efabl  26527  efsubm  26528  qrngbas  27598  ressplusf  33055  ressnm  33056  ressprs  33058  subgmulgcld  33136  ressmulgnn0d  33137  xrge0tsmsd  33166  ress1r  33326  subrdom  33378  subsdrg  33391  idomsubr  33402  xrge0slmod  33440  znfermltl  33458  ressply1evls1  33657  ressasclcl  33663  resssra  33763  drgextlsp  33770  lssdimle  33784  lbslsat  33793  ply1degltdimlem  33799  ply1degltdim  33800  dimkerim  33804  fedgmullem1  33806  fedgmullem2  33807  fedgmul  33808  dimlssid  33809  lvecendof1f1o  33810  sdrgfldext  33827  fldsdrgfldext  33838  fldsdrgfldext2  33839  fldgenfldext  33845  evls1fldgencl  33847  fldextrspunlsplem  33850  fldextrspunlsp  33851  fldextrspunlem1  33852  fldextrspunfld  33853  fldextrspundgle  33855  fldextrspundgdvdslem  33857  fldextrspundgdvds  33858  0ringirng  33866  extdgfialglem1  33869  extdgfialglem2  33870  algextdeglem3  33896  algextdeglem4  33897  algextdeglem8  33901  rtelextdg2lem  33903  rtelextdg2  33904  constrext2chnlem  33927  2sqr3minply  33957  rspecbas  34042  prsssdm  34094  ordtrestNEW  34098  ordtrest2NEW  34100  xrge0iifmhm  34116  esumpfinvallem  34251  sitgaddlemb  34525  prdsbnd2  38043  cnpwstotbnd  38045  repwsmet  38082  rrnequiv  38083  lcdvbase  41966  primrootsunit1  42464  primrootscoprmpow  42466  primrootscoprbij  42469  aks6d1c6lem4  42540  aks6d1c6isolem2  42542  aks6d1c6lem5  42544  aks5lem7  42567  islssfg  43424  lnmlsslnm  43435  pwssplit4  43443  deg1mhm  43554  gsumge0cl  46726  sge0tsms  46735  cnfldsrngbas  48518  amgmlemALT  50159