Theorem eqsstri 3280

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

This proof depends on syntax axioms:   = wceq 1402   C_ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  eqsstrri  3281  ssrab2  3333  ssrab3  3334  rabssab  3337  difdifdirss  3612  ifssun  3655  opabss  4195  brab2ga  4850  relopabi  4905  dmopabss  4993  resss  5087  relres  5091  exse2  5161  rnin  5197  rnxpss  5219  cnvcnvss  5242  dmmptss  5284  cocnvss  5313  fnres  5500  resasplitss  5569  fabexg  5579  f0  5583  fvopab4ndm  5803  ffvresb  5871  isoini2  6025  dmoprabss  6170  elmpocl  6284  elmpom  6474  tposssxp  6520  dftpos4  6534  smores  6563  smores2  6565  iordsmo  6568  swoer  6835  swoord1  6836  swoord2  6837  ecss  6850  ecopovsym  6905  ecopovtrn  6906  ecopover  6907  ecopovsymg  6908  ecopovtrng  6909  ecopoverg  6910  opabfi  7247  sbthlem7  7280  caserel  7428  ctssdccl  7452  pw1on  7586  pinn  7677  niex  7680  ltrelpi  7692  dmaddpi  7693  dmmulpi  7694  enqex  7728  ltrelnq  7733  enq0ex  7807  ltrelpr  7873  enrex  8105  ltrelsr  8106  ltrelre  8201  axaddf  8236  axmulf  8237  ltrelxr  8387  lerelxr  8389  nn0ssre  9572  nn0ssz  9667  rpre  10072  fz1ssfz0  10535  infssuzcldc  10679  swrd00g  11437  cau3  11898  fsum3cvg3  12182  isumshft  12276  explecnv  12291  clim2prod  12325  ntrivcvgap  12334  dvdszrcl  12578  dvdsflip  12637  phimullem  13026  eulerthlemfi  13029  eulerthlemrprm  13030  eulerthlema  13031  eulerthlemh  13032  eulerthlemth  13033  4sqlem1  13190  4sqlem19  13211  ctiunctlemuom  13379  structcnvcnv  13420  fvsetsid  13438  strleun  13511  cntzsgrpcl  14161  dmtopon  15215  lmfval  15385  lmbrf  15407  cnconst2  15425  txuni2  15448  xmeter  15628  ivthinclemex  15834  dvidsslem  15885  dvconstss  15890  dvrecap  15905  ppiqub  16254  lgsquadlemofi  16361  lgsquadlem1  16362  lgsquadlem2  16363  2sqlem7  16406