Theorem eqsstri 3256

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

Syntax hints:   = wceq 1395   C_ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  eqsstrri  3257  ssrab2  3309  ssrab3  3310  rabssab  3312  difdifdirss  3576  ifssun  3617  opabss  4148  brab2ga  4794  relopabi  4847  dmopabss  4935  resss  5029  relres  5033  exse2  5102  rnin  5138  rnxpss  5160  cnvcnvss  5183  dmmptss  5225  cocnvss  5254  fnres  5440  resasplitss  5505  fabexg  5513  f0  5516  ffvresb  5798  isoini2  5943  dmoprabss  6086  elmpocl  6200  tposssxp  6395  dftpos4  6409  smores  6438  smores2  6440  iordsmo  6443  swoer  6708  swoord1  6709  swoord2  6710  ecss  6723  ecopovsym  6778  ecopovtrn  6779  ecopover  6780  ecopovsymg  6781  ecopovtrng  6782  ecopoverg  6783  opabfi  7100  sbthlem7  7130  caserel  7254  ctssdccl  7278  pw1on  7411  pinn  7496  niex  7499  ltrelpi  7511  dmaddpi  7512  dmmulpi  7513  enqex  7547  ltrelnq  7552  enq0ex  7626  ltrelpr  7692  enrex  7924  ltrelsr  7925  ltrelre  8020  axaddf  8055  axmulf  8056  ltrelxr  8207  lerelxr  8209  nn0ssre  9373  nn0ssz  9464  rpre  9856  fz1ssfz0  10313  infssuzcldc  10455  swrd00g  11181  cau3  11626  fsum3cvg3  11907  isumshft  12001  explecnv  12016  clim2prod  12050  ntrivcvgap  12059  dvdszrcl  12303  dvdsflip  12362  phimullem  12747  eulerthlemfi  12750  eulerthlemrprm  12751  eulerthlema  12752  eulerthlemh  12753  eulerthlemth  12754  4sqlem1  12911  4sqlem19  12932  ctiunctlemuom  13007  structcnvcnv  13048  fvsetsid  13066  strleun  13137  dmtopon  14697  lmfval  14867  lmbrf  14889  cnconst2  14907  txuni2  14930  xmeter  15110  ivthinclemex  15316  dvidsslem  15367  dvconstss  15372  dvrecap  15387  lgsquadlemofi  15755  lgsquadlem1  15756  lgsquadlem2  15757  2sqlem7  15800