Theorem sseqtrri 4046

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.)

Hypotheses

Ref	Expression
sseqtrri.1	⊢ 𝐴 ⊆ 𝐵
sseqtrri.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
sseqtrri	⊢ 𝐴 ⊆ 𝐶

Proof of Theorem sseqtrri

Step	Hyp	Ref	Expression
1		sseqtrri.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		sseqtrri.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2749	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	sseqtri 4045	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  eqimss2i  4070  difsssymdif  4282  snsspr1  4839  snsspr2  4840  snsstp1  4841  snsstp2  4842  snsstp3  4843  unissint  4996  iunxdif2  5076  pwpwssunieq  5127  intabs  5367  inxpssres  5717  elopaelxp  5789  opabssxp  5792  dmresi  6081  cnvimass  6111  sofld  6218  cnvcnv  6223  cnvssrndm  6302  sssucid  6475  cnvimainrn  7100  fvclss  7278  dmmpossx  8107  suppun  8225  frrlem12  8338  wfrlem14OLD  8378  tfrlem11  8444  oawordeulem  8610  mapexOLD  8890  trcl  9797  djuunxp  9990  dfac3  10190  cfsuc  10326  isfin4p1  10384  fin23lem11  10386  domtriomlem  10511  ttukeylem1  10578  ttukeylem7  10584  brdom7disj  10600  brdom6disj  10601  fingch  10692  fpwwe2lem12  10711  canthp1lem2  10722  wunex2  10807  wunex3  10810  ressxr  11334  ltrelxr  11351  nnssnn0  12556  un0addcl  12586  un0mulcl  12587  nn0ssxnn0  12628  caubnd  15407  isumclim3  15807  iprodclim3  16048  bpoly4  16107  fprodefsum  16143  znnen  16260  isprm3  16730  phimullem  16826  isstruct2  17196  2strbas  17281  2strop  17282  2strbas1  17285  rngbase  17358  rngplusg  17359  rngmulr  17360  srngbase  17369  srngplusg  17370  srngmulr  17371  srnginvl  17372  lmodbase  17385  lmodplusg  17386  lmodsca  17387  lmodvsca  17388  ipsbase  17396  ipsaddg  17397  ipsmulr  17398  ipssca  17399  ipsvsca  17400  ipsip  17401  phlbase  17406  phlplusg  17407  phlsca  17408  phlvsca  17409  phlip  17410  topgrpbas  17421  topgrpplusg  17422  topgrptset  17423  otpsbas  17436  otpstset  17437  otpsle  17438  odrngbas  17463  odrngplusg  17464  odrngmulr  17465  odrngtset  17466  odrngle  17467  odrngds  17468  homarw  18113  ipoval  18600  ipolerval  18602  eqgfval  19216  cycsubg  19248  symgbas  19413  symgsubmefmndALT  19445  islbs3  21180  cnfldbas  21391  mpocnfldadd  21392  mpocnfldmul  21394  cnfldcj  21396  cnfldtset  21397  cnfldle  21398  cnfldds  21399  cnfldunif  21400  cnfldbasOLD  21406  cnfldaddOLD  21407  cnfldmulOLD  21408  cnfldcjOLD  21409  cnfldtsetOLD  21410  cnfldleOLD  21411  cnflddsOLD  21412  cnfldunifOLD  21413  basdif0  22981  iscldtop  23124  iocpnfordt  23244  icomnfordt  23245  iooordt  23246  cnrest2  23315  cmpcov2  23419  fiuncmp  23433  bwth  23439  indisconn  23447  locfincmp  23555  xkococnlem  23688  hmphdis  23825  uzrest  23926  ufildr  23960  fin1aufil  23961  eltsms  24162  ustval  24232  qtopbaslem  24800  tgqioo  24841  re2ndc  24842  xrhmeo  24996  bndth  25009  pi1xfrcnvlem  25108  ovolficcss  25523  nulmbl2  25590  uniiccdif  25632  opnmbllem  25655  opnmblALT  25657  mbfimaopnlem  25709  i1fima  25732  i1fima2  25733  i1fd  25735  c1liplem1  26055  deg1n0ima  26148  efcvx  26511  dvrelog  26697  dvloglem  26708  logf1o2  26710  dvlog  26711  ressatans  26995  wilthlem3  27131  bday1s  27894  negsproplem2  28079  negsbdaylem  28106  trkgbas  28471  trkgdist  28472  trkgitv  28473  ex-ss  30459  ajfval  30841  ipasslem8  30869  hlimcaui  31268  shsspwh  31278  hhssabloi  31294  hhssnv  31296  hhshsslem1  31299  shunssji  31401  sshhococi  31578  pjoml6i  31621  osumcori  31675  mayete3i  31760  mayetes3i  31761  imaelshi  32090  pjclem1  32227  pjci  32232  mdcompli  32461  dmdcompli  32462  xppreima  32664  gsummpt2co  33031  cycpmrn  33136  evl1deg1  33566  evl1deg2  33567  evl1deg3  33568  circtopn  33783  esumpcvgval  34042  esumcvg  34050  ldgenpisyslem3  34129  elmbfmvol2  34232  sxbrsigalem0  34236  eulerpartlemsv3  34326  ballotlem7  34500  rpsqrtcn  34570  bnj931  34746  bnj1137  34971  subfacp1lem2a  35148  subfacp1lem2b  35149  erdszelem2  35160  kur14lem7  35180  kur14lem9  35182  dfon2lem2  35748  bj-snglsstag  36947  bj-2upln1upl  36990  bj-0int  37067  bj-opabssvv  37116  bj-ccssccbar  37183  bj-ccinftyssccbar  37184  bj-rvecsscvec  37270  icoreelrn  37327  finxpreclem3  37359  imadifss  37555  poimirlem4  37584  poimirlem26  37606  poimirlem27  37607  opnmbllem0  37616  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  volsupnfl  37625  sdclem2  37702  heibor1lem  37769  refrelsredund4  38588  dicval  41133  dvhdimlem  41401  ismrc  42657  mapfzcons1cl  42674  2rexfrabdioph  42752  3rexfrabdioph  42753  4rexfrabdioph  42754  6rexfrabdioph  42755  7rexfrabdioph  42756  rabdiophlem2  42758  jm2.27dlem5  42970  algbase  43135  algaddg  43136  algmulr  43137  algsca  43138  algvsca  43139  intimass2  43617  comptiunov2i  43668  relexp0a  43678  lhe4.4ex1a  44298  iocnct  45458  iccnct  45459  dvcosre  45833  fourierdlem46  46073  fourierdlem57  46084  fourierdlem58  46085  fourierdlem62  46089  fourierdlem102  46129  fourierdlem103  46130  fourierdlem104  46131  fourierdlem114  46141  sge0split  46330  sge0uzfsumgt  46365  hoiprodp1  46509  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  sbgoldbo  47661  usgrexmpl1lem  47836  usgrexmpl2lem  47841  dmmpossx2  48061  ipoglb0  48666  mreclat  48669  aacllem  48895