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  7427  ctssdccl  7451  pw1on  7585  pinn  7676  niex  7679  ltrelpi  7691  dmaddpi  7692  dmmulpi  7693  enqex  7727  ltrelnq  7732  enq0ex  7806  ltrelpr  7872  enrex  8104  ltrelsr  8105  ltrelre  8200  axaddf  8235  axmulf  8236  ltrelxr  8386  lerelxr  8388  nn0ssre  9571  nn0ssz  9666  rpre  10071  fz1ssfz0  10534  infssuzcldc  10678  swrd00g  11435  cau3  11896  fsum3cvg3  12179  isumshft  12273  explecnv  12288  clim2prod  12322  ntrivcvgap  12331  dvdszrcl  12575  dvdsflip  12634  phimullem  13023  eulerthlemfi  13026  eulerthlemrprm  13027  eulerthlema  13028  eulerthlemh  13029  eulerthlemth  13030  4sqlem1  13187  4sqlem19  13208  ctiunctlemuom  13376  structcnvcnv  13417  fvsetsid  13435  strleun  13507  dmtopon  15173  lmfval  15343  lmbrf  15365  cnconst2  15383  txuni2  15406  xmeter  15586  ivthinclemex  15792  dvidsslem  15843  dvconstss  15848  dvrecap  15863  ppiqub  16194  lgsquadlemofi  16293  lgsquadlem1  16294  lgsquadlem2  16295  2sqlem7  16338