Theorem eqsstri 3216

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 3210	. 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  3217  ssrab2  3269  ssrab3  3270  rabssab  3272  difdifdirss  3536  ifssun  3576  opabss  4098  brab2ga  4739  relopabi  4792  dmopabss  4879  resss  4971  relres  4975  exse2  5044  rnin  5080  rnxpss  5102  cnvcnvss  5125  dmmptss  5167  cocnvss  5196  fnres  5375  resasplitss  5438  fabexg  5446  f0  5449  ffvresb  5726  isoini2  5867  dmoprabss  6006  elmpocl  6120  tposssxp  6309  dftpos4  6323  smores  6352  smores2  6354  iordsmo  6357  swoer  6622  swoord1  6623  swoord2  6624  ecss  6637  ecopovsym  6692  ecopovtrn  6693  ecopover  6694  ecopovsymg  6695  ecopovtrng  6696  ecopoverg  6697  opabfi  7001  sbthlem7  7031  caserel  7155  ctssdccl  7179  pw1on  7296  pinn  7379  niex  7382  ltrelpi  7394  dmaddpi  7395  dmmulpi  7396  enqex  7430  ltrelnq  7435  enq0ex  7509  ltrelpr  7575  enrex  7807  ltrelsr  7808  ltrelre  7903  axaddf  7938  axmulf  7939  ltrelxr  8090  lerelxr  8092  nn0ssre  9256  nn0ssz  9347  rpre  9738  fz1ssfz0  10195  infssuzcldc  10328  cau3  11283  fsum3cvg3  11564  isumshft  11658  explecnv  11673  clim2prod  11707  ntrivcvgap  11716  dvdszrcl  11960  dvdsflip  12019  phimullem  12404  eulerthlemfi  12407  eulerthlemrprm  12408  eulerthlema  12409  eulerthlemh  12410  eulerthlemth  12411  4sqlem1  12568  4sqlem19  12589  ctiunctlemuom  12664  structcnvcnv  12705  fvsetsid  12723  strleun  12793  dmtopon  14285  lmfval  14454  lmbrf  14477  cnconst2  14495  txuni2  14518  xmeter  14698  ivthinclemex  14904  dvidsslem  14955  dvconstss  14960  dvrecap  14975  lgsquadlemofi  15343  lgsquadlem1  15344  lgsquadlem2  15345  2sqlem7  15388