Theorem sseqtrri 3984

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 2740	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	sseqtri 3983	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1541   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3919

This theorem is referenced by:  3sstr4i  3986  eqimss2i  3996  difsssymdif  4213  snsspr1  4766  snsspr2  4767  snsstp1  4768  snsstp2  4769  snsstp3  4770  unissint  4922  iunxdif2  5002  pwpwssunieq  5052  intabs  5287  inxpssres  5633  elopaelxp  5706  opabssxp  5708  dmresi  6001  cnvimass  6031  sofld  6134  cnvcnv  6139  cnvssrndm  6218  sssucid  6388  f1imadifssran  6567  cnvimainrn  7000  fvclss  7175  dmmpossx  7998  suppun  8114  frrlem12  8227  tfrlem11  8307  oawordeulem  8469  mapexOLD  8756  trcl  9618  djuunxp  9811  dfac3  10009  cfsuc  10145  isfin4p1  10203  fin23lem11  10205  domtriomlem  10330  ttukeylem1  10397  ttukeylem7  10403  brdom7disj  10419  brdom6disj  10420  fingch  10511  fpwwe2lem12  10530  canthp1lem2  10541  wunex2  10626  wunex3  10629  ressxr  11153  ltrelxr  11170  nnssnn0  12381  un0addcl  12411  un0mulcl  12412  nn0ssxnn0  12454  caubnd  15263  isumclim3  15663  iprodclim3  15904  bpoly4  15963  fprodefsum  15999  znnen  16118  isprm3  16591  phimullem  16687  isstruct2  17057  2strbas  17136  rngbase  17200  rngplusg  17201  rngmulr  17202  srngbase  17211  srngplusg  17212  srngmulr  17213  srnginvl  17214  lmodbase  17227  lmodplusg  17228  lmodsca  17229  lmodvsca  17230  ipsbase  17238  ipsaddg  17239  ipsmulr  17240  ipssca  17241  ipsvsca  17242  ipsip  17243  phlbase  17248  phlplusg  17249  phlsca  17250  phlvsca  17251  phlip  17252  topgrpbas  17263  topgrpplusg  17264  topgrptset  17265  otpsbas  17278  otpstset  17279  otpsle  17280  odrngbas  17305  odrngplusg  17306  odrngmulr  17307  odrngtset  17308  odrngle  17309  odrngds  17310  homarw  17950  ipoval  18433  ipolerval  18435  eqgfval  19086  cycsubg  19118  symgbas  19282  symgsubmefmndALT  19313  islbs3  21090  cnfldbas  21293  mpocnfldadd  21294  mpocnfldmul  21296  cnfldcj  21298  cnfldtset  21299  cnfldle  21300  cnfldds  21301  cnfldunif  21302  cnfldbasOLD  21308  cnfldaddOLD  21309  cnfldmulOLD  21310  cnfldcjOLD  21311  cnfldtsetOLD  21312  cnfldleOLD  21313  cnflddsOLD  21314  cnfldunifOLD  21315  basdif0  22866  iscldtop  23008  iocpnfordt  23128  icomnfordt  23129  iooordt  23130  cnrest2  23199  cmpcov2  23303  fiuncmp  23317  bwth  23323  indisconn  23331  locfincmp  23439  xkococnlem  23572  hmphdis  23709  uzrest  23810  ufildr  23844  fin1aufil  23845  eltsms  24046  ustval  24116  qtopbaslem  24671  tgqioo  24713  re2ndc  24714  xrhmeo  24869  bndth  24882  pi1xfrcnvlem  24981  ovolficcss  25395  nulmbl2  25462  uniiccdif  25504  opnmbllem  25527  opnmblALT  25529  mbfimaopnlem  25581  i1fima  25604  i1fima2  25605  i1fd  25607  c1liplem1  25926  deg1n0ima  26019  efcvx  26384  dvrelog  26571  dvloglem  26582  logf1o2  26584  dvlog  26585  ressatans  26869  wilthlem3  27005  bday1s  27773  negsproplem2  27969  negsbdaylem  27996  onscutlt  28199  onsiso  28203  bdayon  28207  bdayn0p1  28292  trkgbas  28421  trkgdist  28422  trkgitv  28423  ex-ss  30402  ajfval  30784  ipasslem8  30812  hlimcaui  31211  shsspwh  31221  hhssabloi  31237  hhssnv  31239  hhshsslem1  31242  shunssji  31344  sshhococi  31521  pjoml6i  31564  osumcori  31618  mayete3i  31703  mayetes3i  31704  imaelshi  32033  pjclem1  32170  pjci  32175  mdcompli  32404  dmdcompli  32405  xppreima  32622  gsummpt2co  33023  cycpmrn  33107  elrgspnsubrunlem2  33210  evl1deg1  33534  evl1deg2  33535  evl1deg3  33536  circtopn  33845  esumpcvgval  34086  esumcvg  34094  ldgenpisyslem3  34173  elmbfmvol2  34275  sxbrsigalem0  34279  eulerpartlemsv3  34369  ballotlem7  34544  rpsqrtcn  34601  bnj931  34777  bnj1137  35002  fineqvnttrclse  35132  subfacp1lem2a  35212  subfacp1lem2b  35213  erdszelem2  35224  kur14lem7  35244  kur14lem9  35246  dfon2lem2  35817  bj-snglsstag  37014  bj-2upln1upl  37057  bj-0int  37134  bj-opabssvv  37183  bj-ccssccbar  37250  bj-ccinftyssccbar  37251  bj-rvecsscvec  37337  icoreelrn  37394  finxpreclem3  37426  imadifss  37634  poimirlem4  37663  poimirlem26  37685  poimirlem27  37686  opnmbllem0  37695  mblfinlem3  37698  mblfinlem4  37699  ismblfin  37700  volsupnfl  37704  sdclem2  37781  heibor1lem  37848  refrelsredund4  38668  dicval  41214  dvhdimlem  41482  ismrc  42733  mapfzcons1cl  42750  2rexfrabdioph  42828  3rexfrabdioph  42829  4rexfrabdioph  42830  6rexfrabdioph  42831  7rexfrabdioph  42832  rabdiophlem2  42834  jm2.27dlem5  43045  algbase  43206  algaddg  43207  algmulr  43208  algsca  43209  algvsca  43210  intimass2  43687  comptiunov2i  43738  relexp0a  43748  lhe4.4ex1a  44361  iocnct  45579  iccnct  45580  dvcosre  45949  fourierdlem46  46189  fourierdlem57  46200  fourierdlem58  46201  fourierdlem62  46205  fourierdlem102  46245  fourierdlem103  46246  fourierdlem104  46247  fourierdlem114  46257  sge0split  46446  sge0uzfsumgt  46481  hoiprodp1  46625  hoidmvlelem1  46632  hoidmvlelem2  46633  hoidmvlelem3  46634  sbgoldbo  47817  usgrexmpl1lem  48051  usgrexmpl2lem  48056  dmmpossx2  48367  ipoglb0  49024  mreclat  49027  catbas  49257  cathomfval  49258  catcofval  49259  aacllem  49832