Theorem eqsstri 3189

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

Syntax hints:   = wceq 1353   C_ wss 3131

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3137  df-ss 3144

This theorem is referenced by:  eqsstrri  3190  ssrab2  3242  ssrab3  3243  rabssab  3245  difdifdirss  3509  ifssun  3550  opabss  4069  brab2ga  4703  relopabi  4754  dmopabss  4841  resss  4933  relres  4937  exse2  5004  rnin  5040  rnxpss  5062  cnvcnvss  5085  dmmptss  5127  cocnvss  5156  fnres  5334  resasplitss  5397  fabexg  5405  f0  5408  ffvresb  5681  isoini2  5822  dmoprabss  5959  elmpocl  6071  tposssxp  6252  dftpos4  6266  smores  6295  smores2  6297  iordsmo  6300  swoer  6565  swoord1  6566  swoord2  6567  ecss  6578  ecopovsym  6633  ecopovtrn  6634  ecopover  6635  ecopovsymg  6636  ecopovtrng  6637  ecopoverg  6638  sbthlem7  6964  caserel  7088  ctssdccl  7112  pw1on  7227  pinn  7310  niex  7313  ltrelpi  7325  dmaddpi  7326  dmmulpi  7327  enqex  7361  ltrelnq  7366  enq0ex  7440  ltrelpr  7506  enrex  7738  ltrelsr  7739  ltrelre  7834  axaddf  7869  axmulf  7870  ltrelxr  8020  lerelxr  8022  nn0ssre  9182  nn0ssz  9273  rpre  9662  fz1ssfz0  10119  cau3  11126  fsum3cvg3  11406  isumshft  11500  explecnv  11515  clim2prod  11549  ntrivcvgap  11558  dvdszrcl  11801  dvdsflip  11859  infssuzcldc  11954  phimullem  12227  eulerthlemfi  12230  eulerthlemrprm  12231  eulerthlema  12232  eulerthlemh  12233  eulerthlemth  12234  4sqlem1  12388  ctiunctlemuom  12439  structcnvcnv  12480  fvsetsid  12498  strleun  12565  dmtopon  13562  lmfval  13731  lmbrf  13754  cnconst2  13772  txuni2  13795  xmeter  13975  ivthinclemex  14159  dvrecap  14216  2sqlem7  14507