Theorem eqsstri 3260

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

Syntax hints:   = wceq 1398   C_ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  eqsstrri  3261  ssrab2  3313  ssrab3  3314  rabssab  3317  difdifdirss  3581  ifssun  3624  opabss  4158  brab2ga  4807  relopabi  4861  dmopabss  4949  resss  5043  relres  5047  exse2  5117  rnin  5153  rnxpss  5175  cnvcnvss  5198  dmmptss  5240  cocnvss  5269  fnres  5456  resasplitss  5524  fabexg  5532  f0  5536  ffvresb  5818  isoini2  5970  dmoprabss  6113  elmpocl  6227  elmpom  6412  tposssxp  6458  dftpos4  6472  smores  6501  smores2  6503  iordsmo  6506  swoer  6773  swoord1  6774  swoord2  6775  ecss  6788  ecopovsym  6843  ecopovtrn  6844  ecopover  6845  ecopovsymg  6846  ecopovtrng  6847  ecopoverg  6848  opabfi  7175  sbthlem7  7205  caserel  7346  ctssdccl  7370  pw1on  7504  pinn  7589  niex  7592  ltrelpi  7604  dmaddpi  7605  dmmulpi  7606  enqex  7640  ltrelnq  7645  enq0ex  7719  ltrelpr  7785  enrex  8017  ltrelsr  8018  ltrelre  8113  axaddf  8148  axmulf  8149  ltrelxr  8299  lerelxr  8301  nn0ssre  9465  nn0ssz  9558  rpre  9956  fz1ssfz0  10414  infssuzcldc  10558  swrd00g  11296  cau3  11755  fsum3cvg3  12037  isumshft  12131  explecnv  12146  clim2prod  12180  ntrivcvgap  12189  dvdszrcl  12433  dvdsflip  12492  phimullem  12877  eulerthlemfi  12880  eulerthlemrprm  12881  eulerthlema  12882  eulerthlemh  12883  eulerthlemth  12884  4sqlem1  13041  4sqlem19  13062  ctiunctlemuom  13137  structcnvcnv  13178  fvsetsid  13196  strleun  13267  dmtopon  14834  lmfval  15004  lmbrf  15026  cnconst2  15044  txuni2  15067  xmeter  15247  ivthinclemex  15453  dvidsslem  15504  dvconstss  15509  dvrecap  15524  lgsquadlemofi  15895  lgsquadlem1  15896  lgsquadlem2  15897  2sqlem7  15940