Theorem eqsstri 3225

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

Syntax hints:   = wceq 1373   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  eqsstrri  3226  ssrab2  3278  ssrab3  3279  rabssab  3281  difdifdirss  3545  ifssun  3585  opabss  4108  brab2ga  4750  relopabi  4803  dmopabss  4890  resss  4983  relres  4987  exse2  5056  rnin  5092  rnxpss  5114  cnvcnvss  5137  dmmptss  5179  cocnvss  5208  fnres  5392  resasplitss  5455  fabexg  5463  f0  5466  ffvresb  5743  isoini2  5888  dmoprabss  6027  elmpocl  6141  tposssxp  6335  dftpos4  6349  smores  6378  smores2  6380  iordsmo  6383  swoer  6648  swoord1  6649  swoord2  6650  ecss  6663  ecopovsym  6718  ecopovtrn  6719  ecopover  6720  ecopovsymg  6721  ecopovtrng  6722  ecopoverg  6723  opabfi  7035  sbthlem7  7065  caserel  7189  ctssdccl  7213  pw1on  7338  pinn  7422  niex  7425  ltrelpi  7437  dmaddpi  7438  dmmulpi  7439  enqex  7473  ltrelnq  7478  enq0ex  7552  ltrelpr  7618  enrex  7850  ltrelsr  7851  ltrelre  7946  axaddf  7981  axmulf  7982  ltrelxr  8133  lerelxr  8135  nn0ssre  9299  nn0ssz  9390  rpre  9782  fz1ssfz0  10239  infssuzcldc  10378  swrd00g  11102  cau3  11426  fsum3cvg3  11707  isumshft  11801  explecnv  11816  clim2prod  11850  ntrivcvgap  11859  dvdszrcl  12103  dvdsflip  12162  phimullem  12547  eulerthlemfi  12550  eulerthlemrprm  12551  eulerthlema  12552  eulerthlemh  12553  eulerthlemth  12554  4sqlem1  12711  4sqlem19  12732  ctiunctlemuom  12807  structcnvcnv  12848  fvsetsid  12866  strleun  12936  dmtopon  14495  lmfval  14664  lmbrf  14687  cnconst2  14705  txuni2  14728  xmeter  14908  ivthinclemex  15114  dvidsslem  15165  dvconstss  15170  dvrecap  15185  lgsquadlemofi  15553  lgsquadlem1  15554  lgsquadlem2  15555  2sqlem7  15598