Theorem eqsstri 3212

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

Syntax hints:   = wceq 1364   C_ wss 3154

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  eqsstrri  3213  ssrab2  3265  ssrab3  3266  rabssab  3268  difdifdirss  3532  ifssun  3572  opabss  4094  brab2ga  4735  relopabi  4788  dmopabss  4875  resss  4967  relres  4971  exse2  5040  rnin  5076  rnxpss  5098  cnvcnvss  5121  dmmptss  5163  cocnvss  5192  fnres  5371  resasplitss  5434  fabexg  5442  f0  5445  ffvresb  5722  isoini2  5863  dmoprabss  6001  elmpocl  6115  tposssxp  6304  dftpos4  6318  smores  6347  smores2  6349  iordsmo  6352  swoer  6617  swoord1  6618  swoord2  6619  ecss  6632  ecopovsym  6687  ecopovtrn  6688  ecopover  6689  ecopovsymg  6690  ecopovtrng  6691  ecopoverg  6692  opabfi  6994  sbthlem7  7024  caserel  7148  ctssdccl  7172  pw1on  7288  pinn  7371  niex  7374  ltrelpi  7386  dmaddpi  7387  dmmulpi  7388  enqex  7422  ltrelnq  7427  enq0ex  7501  ltrelpr  7567  enrex  7799  ltrelsr  7800  ltrelre  7895  axaddf  7930  axmulf  7931  ltrelxr  8082  lerelxr  8084  nn0ssre  9247  nn0ssz  9338  rpre  9729  fz1ssfz0  10186  cau3  11262  fsum3cvg3  11542  isumshft  11636  explecnv  11651  clim2prod  11685  ntrivcvgap  11694  dvdszrcl  11938  dvdsflip  11996  infssuzcldc  12091  phimullem  12366  eulerthlemfi  12369  eulerthlemrprm  12370  eulerthlema  12371  eulerthlemh  12372  eulerthlemth  12373  4sqlem1  12529  4sqlem19  12550  ctiunctlemuom  12596  structcnvcnv  12637  fvsetsid  12655  strleun  12725  dmtopon  14202  lmfval  14371  lmbrf  14394  cnconst2  14412  txuni2  14435  xmeter  14615  ivthinclemex  14821  dvidsslem  14872  dvconstss  14877  dvrecap  14892  lgsquadlemofi  15233  lgsquadlem1  15234  lgsquadlem2  15235  2sqlem7  15278