Theorem sseqtr4i 3638

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

Hypotheses

Ref	Expression
sseqtr4.1	|- A C_ B
sseqtr4.2	|- C = B

Assertion

Ref	Expression
sseqtr4i	|- A C_ C

Proof of Theorem sseqtr4i

Step	Hyp	Ref	Expression
1		sseqtr4.1	. 2 |- A C_ B
2		sseqtr4.2	. . 3 |- C = B
3	2	eqcomi 2631	. 2 |- B = C
4	1, 3	sseqtri 3637	1 |- A C_ C

Syntax hints:   = wceq 1483   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  eqimss2i  3660  snsspr1  4345  snsspr2  4346  snsstp1  4347  snsstp2  4348  snsstp3  4349  unissint  4501  iunxdif2  4568  pwpwssunieq  4615  intabs  4825  opabssxp  5193  dmresi  5457  cnvimass  5485  ssrnres  5572  sofld  5581  cnvcnv  5586  cnvcnvOLD  5587  cnvssrndm  5657  sssucid  5802  fvclss  6500  dmmpt2ssx  7235  suppun  7315  wfrlem14  7428  tfrlem11  7484  oawordeulem  7634  mapex  7863  trcl  8604  dfac3  8944  cfsuc  9079  fin23lem11  9139  domtriomlem  9264  ttukeylem1  9331  ttukeylem7  9337  brdom7disj  9353  brdom6disj  9354  fingch  9445  fpwwe2lem13  9464  canthp1lem2  9475  wunex2  9560  wunex3  9563  ressxr  10083  ltrelxr  10099  nnssnn0  11295  un0addcl  11326  un0mulcl  11327  nn0ssxnn0  11366  fzssnn  12385  caubnd  14098  isumclim3  14490  iprodclim3  14731  bpoly4  14790  fprodefsum  14825  znnen  14941  isprm3  15396  phimullem  15484  vdwnnlem1  15699  isstruct2  15867  2strbas  15984  2strop  15985  2strbas1  15987  rngbase  16001  rngplusg  16002  rngmulr  16003  srngbase  16009  srngplusg  16010  srngmulr  16011  srnginvl  16012  lmodbase  16018  lmodplusg  16019  lmodsca  16020  lmodvsca  16021  ipsbase  16025  ipsaddg  16026  ipsmulr  16027  ipssca  16028  ipsvsca  16029  ipsip  16030  phlbase  16035  phlplusg  16036  phlsca  16037  phlvsca  16038  phlip  16039  topgrpbas  16043  topgrpplusg  16044  topgrptset  16045  otpsbas  16052  otpstset  16053  otpsle  16054  otpsbasOLD  16056  otpstsetOLD  16057  otpsleOLD  16058  odrngbas  16067  odrngplusg  16068  odrngmulr  16069  odrngtset  16070  odrngle  16071  odrngds  16072  homarw  16696  ipoval  17154  ipolerval  17156  cycsubg  17622  eqgfval  17642  gsumval3  18308  islbs3  19155  cnfldbas  19750  cnfldadd  19751  cnfldmul  19752  cnfldcj  19753  cnfldtset  19754  cnfldle  19755  cnfldds  19756  cnfldunif  19757  basdif0  20757  iscldtop  20899  iocpnfordt  21019  icomnfordt  21020  iooordt  21021  cnrest2  21090  cmpcov2  21193  fiuncmp  21207  bwth  21213  indisconn  21221  locfincmp  21329  xkococnlem  21462  hmphdis  21599  uzrest  21701  ufildr  21735  fin1aufil  21736  eltsms  21936  ustval  22006  qtopbaslem  22562  tgqioo  22603  re2ndc  22604  xrhmeo  22745  bndth  22757  pi1xfrcnvlem  22856  ovolficcss  23238  nulmbl2  23304  uniiccdif  23346  opnmbllem  23369  opnmblALT  23371  mbfimaopnlem  23422  i1fima  23445  i1fima2  23446  i1fd  23448  c1liplem1  23759  deg1n0ima  23849  efcvx  24203  dvrelog  24383  dvloglem  24394  logf1o2  24396  dvlog  24397  ressatans  24661  wilthlem3  24796  trkgbas  25344  trkgdist  25345  trkgitv  25346  ex-ss  27284  ajfval  27664  ipasslem8  27692  hlimcaui  28093  shsspwh  28103  hhssabloi  28119  hhssnv  28121  hhshsslem1  28124  shunssji  28228  sshhococi  28405  pjoml6i  28448  osumcori  28502  mayete3i  28587  mayetes3i  28588  imaelshi  28917  pjclem1  29054  pjci  29059  mdcompli  29288  dmdcompli  29289  xppreima  29449  gsummpt2co  29780  circtopn  29904  esumpcvgval  30140  esumcvg  30148  ldgenpisyslem3  30228  elmbfmvol2  30329  sxbrsigalem0  30333  eulerpartlemsv3  30423  ballotlem7  30597  rpsqrtcn  30671  bnj931  30841  bnj1137  31063  subfacp1lem2a  31162  subfacp1lem2b  31163  erdszelem2  31174  kur14lem7  31194  kur14lem9  31196  dfon2lem2  31689  bj-snglsstag  32969  bj-2upln1upl  33012  bj-0int  33055  bj-ccssccbar  33104  bj-ccinftyssccbar  33105  icoreelrn  33209  finxpreclem3  33230  imadifss  33384  poimirlem4  33413  poimirlem26  33435  poimirlem27  33436  opnmbllem0  33445  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  volsupnfl  33454  sdclem2  33538  heibor1lem  33608  inxpssres  34076  dicval  36465  dvhdimlem  36733  ismrc  37264  mapfzcons1cl  37281  2rexfrabdioph  37360  3rexfrabdioph  37361  4rexfrabdioph  37362  6rexfrabdioph  37363  7rexfrabdioph  37364  rabdiophlem2  37366  jm2.27dlem5  37580  algbase  37748  algaddg  37749  algmulr  37750  algsca  37751  algvsca  37752  intimass2  37947  comptiunov2i  37998  relexp0a  38008  lhe4.4ex1a  38528  iocnct  39767  iccnct  39768  dvcosre  40126  fourierdlem46  40369  fourierdlem57  40380  fourierdlem58  40381  fourierdlem62  40385  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem114  40437  sge0split  40626  sge0uzfsumgt  40661  hoiprodp1  40802  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  sbgoldbo  41675  dmmpt2ssx2  42115  aacllem  42547