Theorem eqsstri 3225

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

Syntax hints:   = wceq 1373   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  eqsstrri  3226  ssrab2  3278  ssrab3  3279  rabssab  3281  difdifdirss  3545  ifssun  3585  opabss  4109  brab2ga  4751  relopabi  4804  dmopabss  4891  resss  4984  relres  4988  exse2  5057  rnin  5093  rnxpss  5115  cnvcnvss  5138  dmmptss  5180  cocnvss  5209  fnres  5394  resasplitss  5457  fabexg  5465  f0  5468  ffvresb  5745  isoini2  5890  dmoprabss  6029  elmpocl  6143  tposssxp  6337  dftpos4  6351  smores  6380  smores2  6382  iordsmo  6385  swoer  6650  swoord1  6651  swoord2  6652  ecss  6665  ecopovsym  6720  ecopovtrn  6721  ecopover  6722  ecopovsymg  6723  ecopovtrng  6724  ecopoverg  6725  opabfi  7037  sbthlem7  7067  caserel  7191  ctssdccl  7215  pw1on  7340  pinn  7424  niex  7427  ltrelpi  7439  dmaddpi  7440  dmmulpi  7441  enqex  7475  ltrelnq  7480  enq0ex  7554  ltrelpr  7620  enrex  7852  ltrelsr  7853  ltrelre  7948  axaddf  7983  axmulf  7984  ltrelxr  8135  lerelxr  8137  nn0ssre  9301  nn0ssz  9392  rpre  9784  fz1ssfz0  10241  infssuzcldc  10380  swrd00g  11105  cau3  11459  fsum3cvg3  11740  isumshft  11834  explecnv  11849  clim2prod  11883  ntrivcvgap  11892  dvdszrcl  12136  dvdsflip  12195  phimullem  12580  eulerthlemfi  12583  eulerthlemrprm  12584  eulerthlema  12585  eulerthlemh  12586  eulerthlemth  12587  4sqlem1  12744  4sqlem19  12765  ctiunctlemuom  12840  structcnvcnv  12881  fvsetsid  12899  strleun  12969  dmtopon  14528  lmfval  14697  lmbrf  14720  cnconst2  14738  txuni2  14761  xmeter  14941  ivthinclemex  15147  dvidsslem  15198  dvconstss  15203  dvrecap  15218  lgsquadlemofi  15586  lgsquadlem1  15587  lgsquadlem2  15588  2sqlem7  15631