Theorem eqsstri 3201

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

Hypotheses

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

Assertion

Ref	Expression
eqsstri	|- A C_ C

Proof of Theorem eqsstri

Step	Hyp	Ref	Expression
1		eqsstr.2	. 2 |- B C_ C
2		eqsstr.1	. . 3 |- A = B
3	2	sseq1i 3195	. 2 |- ( A C_ C <-> B C_ C )
4	1, 3	mpbir 146	1 |- A C_ C

Syntax hints:   = wceq 1363   C_ wss 3143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2170

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2175  df-cleq 2181  df-clel 2184  df-in 3149  df-ss 3156

This theorem is referenced by:  eqsstrri  3202  ssrab2  3254  ssrab3  3255  rabssab  3257  difdifdirss  3521  ifssun  3562  opabss  4081  brab2ga  4715  relopabi  4766  dmopabss  4853  resss  4945  relres  4949  exse2  5016  rnin  5052  rnxpss  5074  cnvcnvss  5097  dmmptss  5139  cocnvss  5168  fnres  5346  resasplitss  5409  fabexg  5417  f0  5420  ffvresb  5694  isoini2  5835  dmoprabss  5972  elmpocl  6085  tposssxp  6267  dftpos4  6281  smores  6310  smores2  6312  iordsmo  6315  swoer  6580  swoord1  6581  swoord2  6582  ecss  6593  ecopovsym  6648  ecopovtrn  6649  ecopover  6650  ecopovsymg  6651  ecopovtrng  6652  ecopoverg  6653  sbthlem7  6979  caserel  7103  ctssdccl  7127  pw1on  7242  pinn  7325  niex  7328  ltrelpi  7340  dmaddpi  7341  dmmulpi  7342  enqex  7376  ltrelnq  7381  enq0ex  7455  ltrelpr  7521  enrex  7753  ltrelsr  7754  ltrelre  7849  axaddf  7884  axmulf  7885  ltrelxr  8035  lerelxr  8037  nn0ssre  9197  nn0ssz  9288  rpre  9677  fz1ssfz0  10134  cau3  11141  fsum3cvg3  11421  isumshft  11515  explecnv  11530  clim2prod  11564  ntrivcvgap  11573  dvdszrcl  11816  dvdsflip  11874  infssuzcldc  11969  phimullem  12242  eulerthlemfi  12245  eulerthlemrprm  12246  eulerthlema  12247  eulerthlemh  12248  eulerthlemth  12249  4sqlem1  12403  ctiunctlemuom  12454  structcnvcnv  12495  fvsetsid  12513  strleun  12581  dmtopon  13906  lmfval  14075  lmbrf  14098  cnconst2  14116  txuni2  14139  xmeter  14319  ivthinclemex  14503  dvrecap  14560  2sqlem7  14851