Theorem eqsstri 3259

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

Syntax hints:   = wceq 1397   C_ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  eqsstrri  3260  ssrab2  3312  ssrab3  3313  rabssab  3315  difdifdirss  3579  ifssun  3620  opabss  4153  brab2ga  4801  relopabi  4855  dmopabss  4943  resss  5037  relres  5041  exse2  5110  rnin  5146  rnxpss  5168  cnvcnvss  5191  dmmptss  5233  cocnvss  5262  fnres  5449  resasplitss  5516  fabexg  5524  f0  5528  ffvresb  5811  isoini2  5963  dmoprabss  6106  elmpocl  6220  elmpom  6406  tposssxp  6418  dftpos4  6432  smores  6461  smores2  6463  iordsmo  6466  swoer  6733  swoord1  6734  swoord2  6735  ecss  6748  ecopovsym  6803  ecopovtrn  6804  ecopover  6805  ecopovsymg  6806  ecopovtrng  6807  ecopoverg  6808  opabfi  7135  sbthlem7  7165  caserel  7289  ctssdccl  7313  pw1on  7447  pinn  7532  niex  7535  ltrelpi  7547  dmaddpi  7548  dmmulpi  7549  enqex  7583  ltrelnq  7588  enq0ex  7662  ltrelpr  7728  enrex  7960  ltrelsr  7961  ltrelre  8056  axaddf  8091  axmulf  8092  ltrelxr  8243  lerelxr  8245  nn0ssre  9409  nn0ssz  9500  rpre  9898  fz1ssfz0  10355  infssuzcldc  10499  swrd00g  11237  cau3  11696  fsum3cvg3  11978  isumshft  12072  explecnv  12087  clim2prod  12121  ntrivcvgap  12130  dvdszrcl  12374  dvdsflip  12433  phimullem  12818  eulerthlemfi  12821  eulerthlemrprm  12822  eulerthlema  12823  eulerthlemh  12824  eulerthlemth  12825  4sqlem1  12982  4sqlem19  13003  ctiunctlemuom  13078  structcnvcnv  13119  fvsetsid  13137  strleun  13208  dmtopon  14774  lmfval  14944  lmbrf  14966  cnconst2  14984  txuni2  15007  xmeter  15187  ivthinclemex  15393  dvidsslem  15444  dvconstss  15449  dvrecap  15464  lgsquadlemofi  15832  lgsquadlem1  15833  lgsquadlem2  15834  2sqlem7  15877