Theorem eqsstri 3233

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

Syntax hints:   = wceq 1373   C_ wss 3174

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187

This theorem is referenced by:  eqsstrri  3234  ssrab2  3286  ssrab3  3287  rabssab  3289  difdifdirss  3553  ifssun  3594  opabss  4124  brab2ga  4768  relopabi  4821  dmopabss  4909  resss  5002  relres  5006  exse2  5075  rnin  5111  rnxpss  5133  cnvcnvss  5156  dmmptss  5198  cocnvss  5227  fnres  5412  resasplitss  5477  fabexg  5485  f0  5488  ffvresb  5766  isoini2  5911  dmoprabss  6050  elmpocl  6164  tposssxp  6358  dftpos4  6372  smores  6401  smores2  6403  iordsmo  6406  swoer  6671  swoord1  6672  swoord2  6673  ecss  6686  ecopovsym  6741  ecopovtrn  6742  ecopover  6743  ecopovsymg  6744  ecopovtrng  6745  ecopoverg  6746  opabfi  7061  sbthlem7  7091  caserel  7215  ctssdccl  7239  pw1on  7372  pinn  7457  niex  7460  ltrelpi  7472  dmaddpi  7473  dmmulpi  7474  enqex  7508  ltrelnq  7513  enq0ex  7587  ltrelpr  7653  enrex  7885  ltrelsr  7886  ltrelre  7981  axaddf  8016  axmulf  8017  ltrelxr  8168  lerelxr  8170  nn0ssre  9334  nn0ssz  9425  rpre  9817  fz1ssfz0  10274  infssuzcldc  10415  swrd00g  11140  cau3  11541  fsum3cvg3  11822  isumshft  11916  explecnv  11931  clim2prod  11965  ntrivcvgap  11974  dvdszrcl  12218  dvdsflip  12277  phimullem  12662  eulerthlemfi  12665  eulerthlemrprm  12666  eulerthlema  12667  eulerthlemh  12668  eulerthlemth  12669  4sqlem1  12826  4sqlem19  12847  ctiunctlemuom  12922  structcnvcnv  12963  fvsetsid  12981  strleun  13051  dmtopon  14610  lmfval  14779  lmbrf  14802  cnconst2  14820  txuni2  14843  xmeter  15023  ivthinclemex  15229  dvidsslem  15280  dvconstss  15285  dvrecap  15300  lgsquadlemofi  15668  lgsquadlem1  15669  lgsquadlem2  15670  2sqlem7  15713