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  3499  ifssun  3540  opabss  4053  brab2ga  4686  relopabi  4737  dmopabss  4823  resss  4915  relres  4919  exse2  4985  rnin  5020  rnxpss  5042  cnvcnvss  5065  dmmptss  5107  cocnvss  5136  fnres  5314  resasplitss  5377  fabexg  5385  f0  5388  ffvresb  5659  isoini2  5798  dmoprabss  5935  elmpocl  6047  tposssxp  6228  dftpos4  6242  smores  6271  smores2  6273  iordsmo  6276  swoer  6541  swoord1  6542  swoord2  6543  ecss  6554  ecopovsym  6609  ecopovtrn  6610  ecopover  6611  ecopovsymg  6612  ecopovtrng  6613  ecopoverg  6614  sbthlem7  6940  caserel  7064  ctssdccl  7088  pw1on  7203  pinn  7271  niex  7274  ltrelpi  7286  dmaddpi  7287  dmmulpi  7288  enqex  7322  ltrelnq  7327  enq0ex  7401  ltrelpr  7467  enrex  7699  ltrelsr  7700  ltrelre  7795  axaddf  7830  axmulf  7831  ltrelxr  7980  lerelxr  7982  nn0ssre  9139  nn0ssz  9230  rpre  9617  fz1ssfz0  10073  cau3  11079  fsum3cvg3  11359  isumshft  11453  explecnv  11468  clim2prod  11502  ntrivcvgap  11511  dvdszrcl  11754  dvdsflip  11811  infssuzcldc  11906  phimullem  12179  eulerthlemfi  12182  eulerthlemrprm  12183  eulerthlema  12184  eulerthlemh  12185  eulerthlemth  12186  4sqlem1  12340  ctiunctlemuom  12391  structcnvcnv  12432  fvsetsid  12450  strleun  12507  dmtopon  12815  lmfval  12986  lmbrf  13009  cnconst2  13027  txuni2  13050  xmeter  13230  ivthinclemex  13414  dvrecap  13471  2sqlem7  13751