Theorem eqsstri 3134

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

Syntax hints:   = wceq 1332   C_ wss 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3082  df-ss 3089

This theorem is referenced by:  eqsstrri  3135  ssrab2  3187  rabssab  3189  difdifdirss  3452  opabss  4000  brab2ga  4622  relopabi  4673  dmopabss  4759  resss  4851  relres  4855  exse2  4921  rnin  4956  rnxpss  4978  cnvcnvss  5001  dmmptss  5043  cocnvss  5072  fnres  5247  resasplitss  5310  fabexg  5318  f0  5321  ffvresb  5591  isoini2  5728  dmoprabss  5861  elmpocl  5976  tposssxp  6154  dftpos4  6168  smores  6197  smores2  6199  iordsmo  6202  swoer  6465  swoord1  6466  swoord2  6467  ecss  6478  ecopovsym  6533  ecopovtrn  6534  ecopover  6535  ecopovsymg  6536  ecopovtrng  6537  ecopoverg  6538  sbthlem7  6859  caserel  6980  ctssdccl  7004  pinn  7141  niex  7144  ltrelpi  7156  dmaddpi  7157  dmmulpi  7158  enqex  7192  ltrelnq  7197  enq0ex  7271  ltrelpr  7337  enrex  7569  ltrelsr  7570  ltrelre  7665  axaddf  7700  axmulf  7701  ltrelxr  7849  lerelxr  7851  nn0ssre  9005  nn0ssz  9096  rpre  9477  fz1ssfz0  9928  cau3  10919  fsum3cvg3  11197  isumshft  11291  explecnv  11306  clim2prod  11340  ntrivcvgap  11349  dvdszrcl  11534  dvdsflip  11585  infssuzcldc  11680  phimullem  11937  ctiunctlemuom  11985  structcnvcnv  12014  fvsetsid  12032  strleun  12087  dmtopon  12229  lmfval  12400  lmbrf  12423  cnconst2  12441  txuni2  12464  xmeter  12644  ivthinclemex  12828  dvrecap  12885