Theorem eqsstri 3215

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

Syntax hints:   = wceq 1364   C_ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  eqsstrri  3216  ssrab2  3268  ssrab3  3269  rabssab  3271  difdifdirss  3535  ifssun  3575  opabss  4097  brab2ga  4738  relopabi  4791  dmopabss  4878  resss  4970  relres  4974  exse2  5043  rnin  5079  rnxpss  5101  cnvcnvss  5124  dmmptss  5166  cocnvss  5195  fnres  5374  resasplitss  5437  fabexg  5445  f0  5448  ffvresb  5725  isoini2  5866  dmoprabss  6004  elmpocl  6118  tposssxp  6307  dftpos4  6321  smores  6350  smores2  6352  iordsmo  6355  swoer  6620  swoord1  6621  swoord2  6622  ecss  6635  ecopovsym  6690  ecopovtrn  6691  ecopover  6692  ecopovsymg  6693  ecopovtrng  6694  ecopoverg  6695  opabfi  6999  sbthlem7  7029  caserel  7153  ctssdccl  7177  pw1on  7293  pinn  7376  niex  7379  ltrelpi  7391  dmaddpi  7392  dmmulpi  7393  enqex  7427  ltrelnq  7432  enq0ex  7506  ltrelpr  7572  enrex  7804  ltrelsr  7805  ltrelre  7900  axaddf  7935  axmulf  7936  ltrelxr  8087  lerelxr  8089  nn0ssre  9253  nn0ssz  9344  rpre  9735  fz1ssfz0  10192  infssuzcldc  10325  cau3  11280  fsum3cvg3  11561  isumshft  11655  explecnv  11670  clim2prod  11704  ntrivcvgap  11713  dvdszrcl  11957  dvdsflip  12016  phimullem  12393  eulerthlemfi  12396  eulerthlemrprm  12397  eulerthlema  12398  eulerthlemh  12399  eulerthlemth  12400  4sqlem1  12557  4sqlem19  12578  ctiunctlemuom  12653  structcnvcnv  12694  fvsetsid  12712  strleun  12782  dmtopon  14259  lmfval  14428  lmbrf  14451  cnconst2  14469  txuni2  14492  xmeter  14672  ivthinclemex  14878  dvidsslem  14929  dvconstss  14934  dvrecap  14949  lgsquadlemofi  15317  lgsquadlem1  15318  lgsquadlem2  15319  2sqlem7  15362