Theorem eqsstri 3179

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

Syntax hints:   = wceq 1348   C_ wss 3121

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  eqsstrri  3180  ssrab2  3232  ssrab3  3233  rabssab  3235  difdifdirss  3498  ifssun  3539  opabss  4051  brab2ga  4684  relopabi  4735  dmopabss  4821  resss  4913  relres  4917  exse2  4983  rnin  5018  rnxpss  5040  cnvcnvss  5063  dmmptss  5105  cocnvss  5134  fnres  5312  resasplitss  5375  fabexg  5383  f0  5386  ffvresb  5657  isoini2  5796  dmoprabss  5933  elmpocl  6045  tposssxp  6226  dftpos4  6240  smores  6269  smores2  6271  iordsmo  6274  swoer  6539  swoord1  6540  swoord2  6541  ecss  6552  ecopovsym  6607  ecopovtrn  6608  ecopover  6609  ecopovsymg  6610  ecopovtrng  6611  ecopoverg  6612  sbthlem7  6938  caserel  7062  ctssdccl  7086  pw1on  7196  pinn  7264  niex  7267  ltrelpi  7279  dmaddpi  7280  dmmulpi  7281  enqex  7315  ltrelnq  7320  enq0ex  7394  ltrelpr  7460  enrex  7692  ltrelsr  7693  ltrelre  7788  axaddf  7823  axmulf  7824  ltrelxr  7973  lerelxr  7975  nn0ssre  9132  nn0ssz  9223  rpre  9610  fz1ssfz0  10066  cau3  11072  fsum3cvg3  11352  isumshft  11446  explecnv  11461  clim2prod  11495  ntrivcvgap  11504  dvdszrcl  11747  dvdsflip  11804  infssuzcldc  11899  phimullem  12172  eulerthlemfi  12175  eulerthlemrprm  12176  eulerthlema  12177  eulerthlemh  12178  eulerthlemth  12179  4sqlem1  12333  ctiunctlemuom  12384  structcnvcnv  12425  fvsetsid  12443  strleun  12500  dmtopon  12780  lmfval  12951  lmbrf  12974  cnconst2  12992  txuni2  13015  xmeter  13195  ivthinclemex  13379  dvrecap  13436  2sqlem7  13716