Theorem eqsstri 3124

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 3118	. 2 |- ( A C_ C <-> B C_ C )
4	1, 3	mpbir 145	1 |- A C_ C

Syntax hints:   = wceq 1331   C_ wss 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-in 3072  df-ss 3079

This theorem is referenced by:  eqsstrri  3125  ssrab2  3177  rabssab  3179  difdifdirss  3442  opabss  3987  brab2ga  4609  relopabi  4660  dmopabss  4746  resss  4838  relres  4842  exse2  4908  rnin  4943  rnxpss  4965  cnvcnvss  4988  dmmptss  5030  cocnvss  5059  fnres  5234  resasplitss  5297  fabexg  5305  f0  5308  ffvresb  5576  isoini2  5713  dmoprabss  5846  elmpocl  5961  tposssxp  6139  dftpos4  6153  smores  6182  smores2  6184  iordsmo  6187  swoer  6450  swoord1  6451  swoord2  6452  ecss  6463  ecopovsym  6518  ecopovtrn  6519  ecopover  6520  ecopovsymg  6521  ecopovtrng  6522  ecopoverg  6523  sbthlem7  6844  caserel  6965  ctssdccl  6989  pinn  7110  niex  7113  ltrelpi  7125  dmaddpi  7126  dmmulpi  7127  enqex  7161  ltrelnq  7166  enq0ex  7240  ltrelpr  7306  enrex  7538  ltrelsr  7539  ltrelre  7634  axaddf  7669  axmulf  7670  ltrelxr  7818  lerelxr  7820  nn0ssre  8974  nn0ssz  9065  rpre  9441  fz1ssfz0  9890  cau3  10880  fsum3cvg3  11158  isumshft  11252  explecnv  11267  clim2prod  11301  ntrivcvgap  11310  dvdszrcl  11487  dvdsflip  11538  infssuzcldc  11633  phimullem  11890  ctiunctlemuom  11938  structcnvcnv  11964  fvsetsid  11982  strleun  12037  dmtopon  12179  lmfval  12350  lmbrf  12373  cnconst2  12391  txuni2  12414  xmeter  12594  ivthinclemex  12778  dvrecap  12835