Theorem eqsstri 3272

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

Syntax hints:   = wceq 1398   C_ wss 3213

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3219  df-ss 3226

This theorem is referenced by:  eqsstrri  3273  ssrab2  3325  ssrab3  3326  rabssab  3329  difdifdirss  3596  ifssun  3639  opabss  4176  brab2ga  4827  relopabi  4882  dmopabss  4970  resss  5064  relres  5068  exse2  5138  rnin  5174  rnxpss  5196  cnvcnvss  5219  dmmptss  5261  cocnvss  5290  fnres  5477  resasplitss  5546  fabexg  5556  f0  5560  ffvresb  5842  isoini2  5994  dmoprabss  6137  elmpocl  6251  elmpom  6436  tposssxp  6482  dftpos4  6496  smores  6525  smores2  6527  iordsmo  6530  swoer  6797  swoord1  6798  swoord2  6799  ecss  6812  ecopovsym  6867  ecopovtrn  6868  ecopover  6869  ecopovsymg  6870  ecopovtrng  6871  ecopoverg  6872  opabfi  7202  sbthlem7  7235  caserel  7380  ctssdccl  7404  pw1on  7538  pinn  7626  niex  7629  ltrelpi  7641  dmaddpi  7642  dmmulpi  7643  enqex  7677  ltrelnq  7682  enq0ex  7756  ltrelpr  7822  enrex  8054  ltrelsr  8055  ltrelre  8150  axaddf  8185  axmulf  8186  ltrelxr  8336  lerelxr  8338  nn0ssre  9502  nn0ssz  9597  rpre  9996  fz1ssfz0  10455  infssuzcldc  10599  swrd00g  11345  cau3  11804  fsum3cvg3  12086  isumshft  12180  explecnv  12195  clim2prod  12229  ntrivcvgap  12238  dvdszrcl  12482  dvdsflip  12541  phimullem  12926  eulerthlemfi  12929  eulerthlemrprm  12930  eulerthlema  12931  eulerthlemh  12932  eulerthlemth  12933  4sqlem1  13090  4sqlem19  13111  ctiunctlemuom  13204  structcnvcnv  13245  fvsetsid  13263  strleun  13334  dmtopon  14905  lmfval  15075  lmbrf  15097  cnconst2  15115  txuni2  15138  xmeter  15318  ivthinclemex  15524  dvidsslem  15575  dvconstss  15580  dvrecap  15595  lgsquadlemofi  15966  lgsquadlem1  15967  lgsquadlem2  15968  2sqlem7  16011