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  4196  brab2ga  4852  relopabi  4907  dmopabss  4995  resss  5089  relres  5093  exse2  5164  rnin  5200  rnxpss  5222  cnvcnvss  5245  dmmptss  5287  cocnvss  5316  fnres  5503  resasplitss  5572  fabexg  5582  f0  5586  fvopab4ndm  5806  ffvresb  5874  isoini2  6028  dmoprabss  6173  elmpocl  6287  elmpom  6478  tposssxp  6524  dftpos4  6538  smores  6567  smores2  6569  iordsmo  6572  swoer  6839  swoord1  6840  swoord2  6841  ecss  6854  ecopovsym  6909  ecopovtrn  6910  ecopover  6911  ecopovsymg  6912  ecopovtrng  6913  ecopoverg  6914  opabfi  7251  sbthlem7  7285  caserel  7433  ctssdccl  7457  pw1on  7591  pinn  7682  niex  7685  ltrelpi  7697  dmaddpi  7698  dmmulpi  7699  enqex  7733  ltrelnq  7738  enq0ex  7812  ltrelpr  7878  enrex  8110  ltrelsr  8111  ltrelre  8206  axaddf  8241  axmulf  8242  ltrelxr  8392  lerelxr  8394  nn0ssre  9578  nn0ssz  9673  rpre  10078  fz1ssfz0  10541  infssuzcldc  10685  swrd00g  11443  cau3  11904  fsum3cvg3  12188  isumshft  12282  explecnv  12297  clim2prod  12331  ntrivcvgap  12340  dvdszrcl  12584  dvdsflip  12643  phimullem  13032  eulerthlemfi  13035  eulerthlemrprm  13036  eulerthlema  13037  eulerthlemh  13038  eulerthlemth  13039  4sqlem1  13196  4sqlem19  13217  ctiunctlemuom  13385  structcnvcnv  13426  fvsetsid  13444  strleun  13517  cntzsgrpcl  14167  dmtopon  15249  lmfval  15419  lmbrf  15441  cnconst2  15459  txuni2  15482  xmeter  15662  ivthinclemex  15868  dvidsslem  15919  dvconstss  15924  dvrecap  15939  ppiqub  16293  lgsquadlemofi  16400  lgsquadlem1  16401  lgsquadlem2  16402  2sqlem7  16445