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  5507  fabexg  5515  f0  5518  ffvresb  5800  isoini2  5949  dmoprabss  6092  elmpocl  6206  tposssxp  6401  dftpos4  6415  smores  6444  smores2  6446  iordsmo  6449  swoer  6716  swoord1  6717  swoord2  6718  ecss  6731  ecopovsym  6786  ecopovtrn  6787  ecopover  6788  ecopovsymg  6789  ecopovtrng  6790  ecopoverg  6791  opabfi  7111  sbthlem7  7141  caserel  7265  ctssdccl  7289  pw1on  7422  pinn  7507  niex  7510  ltrelpi  7522  dmaddpi  7523  dmmulpi  7524  enqex  7558  ltrelnq  7563  enq0ex  7637  ltrelpr  7703  enrex  7935  ltrelsr  7936  ltrelre  8031  axaddf  8066  axmulf  8067  ltrelxr  8218  lerelxr  8220  nn0ssre  9384  nn0ssz  9475  rpre  9868  fz1ssfz0  10325  infssuzcldc  10467  swrd00g  11197  cau3  11642  fsum3cvg3  11923  isumshft  12017  explecnv  12032  clim2prod  12066  ntrivcvgap  12075  dvdszrcl  12319  dvdsflip  12378  phimullem  12763  eulerthlemfi  12766  eulerthlemrprm  12767  eulerthlema  12768  eulerthlemh  12769  eulerthlemth  12770  4sqlem1  12927  4sqlem19  12948  ctiunctlemuom  13023  structcnvcnv  13064  fvsetsid  13082  strleun  13153  dmtopon  14713  lmfval  14883  lmbrf  14905  cnconst2  14923  txuni2  14946  xmeter  15126  ivthinclemex  15332  dvidsslem  15383  dvconstss  15388  dvrecap  15403  lgsquadlemofi  15771  lgsquadlem1  15772  lgsquadlem2  15773  2sqlem7  15816