Theorem eqsstri 3216

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

Syntax hints:   = wceq 1364   C_ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  eqsstrri  3217  ssrab2  3269  ssrab3  3270  rabssab  3272  difdifdirss  3536  ifssun  3576  opabss  4098  brab2ga  4739  relopabi  4792  dmopabss  4879  resss  4971  relres  4975  exse2  5044  rnin  5080  rnxpss  5102  cnvcnvss  5125  dmmptss  5167  cocnvss  5196  fnres  5377  resasplitss  5440  fabexg  5448  f0  5451  ffvresb  5728  isoini2  5869  dmoprabss  6008  elmpocl  6122  tposssxp  6316  dftpos4  6330  smores  6359  smores2  6361  iordsmo  6364  swoer  6629  swoord1  6630  swoord2  6631  ecss  6644  ecopovsym  6699  ecopovtrn  6700  ecopover  6701  ecopovsymg  6702  ecopovtrng  6703  ecopoverg  6704  opabfi  7008  sbthlem7  7038  caserel  7162  ctssdccl  7186  pw1on  7309  pinn  7393  niex  7396  ltrelpi  7408  dmaddpi  7409  dmmulpi  7410  enqex  7444  ltrelnq  7449  enq0ex  7523  ltrelpr  7589  enrex  7821  ltrelsr  7822  ltrelre  7917  axaddf  7952  axmulf  7953  ltrelxr  8104  lerelxr  8106  nn0ssre  9270  nn0ssz  9361  rpre  9752  fz1ssfz0  10209  infssuzcldc  10342  cau3  11297  fsum3cvg3  11578  isumshft  11672  explecnv  11687  clim2prod  11721  ntrivcvgap  11730  dvdszrcl  11974  dvdsflip  12033  phimullem  12418  eulerthlemfi  12421  eulerthlemrprm  12422  eulerthlema  12423  eulerthlemh  12424  eulerthlemth  12425  4sqlem1  12582  4sqlem19  12603  ctiunctlemuom  12678  structcnvcnv  12719  fvsetsid  12737  strleun  12807  dmtopon  14343  lmfval  14512  lmbrf  14535  cnconst2  14553  txuni2  14576  xmeter  14756  ivthinclemex  14962  dvidsslem  15013  dvconstss  15018  dvrecap  15033  lgsquadlemofi  15401  lgsquadlem1  15402  lgsquadlem2  15403  2sqlem7  15446