Theorem ressbas2 17460

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  Vcvv 3454   ⊆ wss 3900   ∩ cin 4092  ‘cfv 6566  (class class class)co 7451  Basecbs 17431   ↾_s cress 17452

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-cnex 11295  ax-1cn 11297  ax-addcl 11299

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-ov 7454  df-oprab 7455  df-mpo 7456  df-om 7912  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-nn 12376  df-sets 17386  df-slot 17404  df-ndx 17416  df-base 17432  df-ress 17453

This theorem is used by:  rescbas  18054  fullresc  18076  resssetc  18317  yoniso  18509  issstrmgm  18881  idressidex0  18910  idressidex  18911  idressid  18912  gsumress  18921  issubmgm2  18942  submgmbas  18948  resmgmhm  18950  issubmnd  19003  ress0gOLD  19005  submnd0OLD  19007  submbas  19060  resmhm  19066  resgrpplusfrn  19211  ressmulgnn  19336  ressmulgnn0  19337  ressmulgnnd  19338  subgbas  19390  issubg2  19402  resghm  19496  symgbas  19637  finodsubmsubg  19832  submod  19834  cntrcmnd  20107  ringidss  20557  unitgrpbas  20663  isdrng2  21048  isdrng3lem0  21055  drngid2  21061  isdrngd  21073  isdrngdOLD  21075  sdrgbas  21102  cntzsdrg  21110  subdrgint  21111  primefld  21113  islss3  21285  lsslss  21287  lsslsp  21341  reslmhm  21378  2idlbas  21608  rng2idl1cntr  21652  cnmsubglem  21790  nn0srg  21797  rge0srg  21798  xrs1mnd  21800  xrs10  21801  xrs1cmn  21802  xrge0subm  21803  xrge0cmn  21804  zringbas  21813  expghm  21836  fermltlchr  21890  cnmsgnbas  21939  psgnghm  21941  rebase  21967  dsmmbase  22096  dsmmval2  22097  lsslindf  22191  lsslinds  22192  islinds3  22195  resspsrbas  22336  mplbas  22352  ressmplbas  22391  evlssca  22458  mpfconst  22473  mpfind  22479  ply1bas  22568  ressply1bas  22601  evls1sca  22696  evls1fpws  22742  evls1vsca  22746  asclply1subcl  22747  evls1maplmhm  22750  m2cpmrngiso  23131  ressusp  24638  imasdsf1olem  24747  xrge0gsumle  25208  xrge0tsms  25209  cmssmscld  25726  cmsss  25727  minveclem3a  25803  efabl  26935  efsubm  26936  qrngbas  28003  ressplusf  33620  ressnm  33621  ressprs  33623  subgmulgcld  33703  ressmulgnn0d  33704  xrge0tsmsd  33733  ress1r  33892  subrdom  33945  subsdrg  33964  idomsubr  33975  xrge0slmod  34013  znfermltl  34026  ressply1evls1  34200  ressasclcl  34206  evls1rgspncl  34248  resssra  34330  drgextlsp  34337  lssdimle  34351  lbslsat  34359  ply1degltdimlem  34365  ply1degltdim  34366  dimkerim  34370  fedgmullem1  34372  fedgmullem2  34373  fedgmul  34374  dimlssid  34375  lvecendof1f1o  34376  sdrgfldext  34393  fldsdrgfldext  34404  fldsdrgfldext2  34405  fldgenfldext  34411  evls1fldgencl  34413  fldextrspunlsplem  34416  fldextrspunlsp  34417  fldextrspunlem1  34418  fldextrspunfld  34419  fldextrspundgle  34421  fldextrspundgdvdslem  34423  fldextrspundgdvds  34424  0ringirng  34432  extdgfialglem1  34435  extdgfialglem2  34436  algextdeglem3  34462  algextdeglem4  34463  algextdeglem8  34467  rtelextdg2lem  34469  rtelextdg2  34470  constrext2chnlem  34493  2sqr3minply  34523  rspecbas  34608  prsssdm  34660  ordtrestNEW  34664  ordtrest2NEW  34666  xrge0iifmhm  34682  esumpfinvallem  34817  sitgaddlemb  35091  prdsbnd2  38995  cnpwstotbnd  38997  repwsmet  39034  rrnequiv  39035  lcdvbase  42916  primrootsunit1  43413  primrootscoprmpow  43415  primrootscoprbij  43418  aks6d1c6lem4  43489  aks6d1c6isolem2  43491  aks6d1c6lem5  43493  aks5lem7  43516  islssfg  44338  lnmlsslnm  44349  pwssplit4  44357  deg1mhm  44463  gsumge0cl  47654  sge0tsms  47663  cnfldsrngbas  49531  amgmlemALT  51416