Theorem eqsstri 3259

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

Syntax hints:   = wceq 1397   C_ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  eqsstrri  3260  ssrab2  3312  ssrab3  3313  rabssab  3315  difdifdirss  3579  ifssun  3620  opabss  4153  brab2ga  4801  relopabi  4855  dmopabss  4943  resss  5037  relres  5041  exse2  5110  rnin  5146  rnxpss  5168  cnvcnvss  5191  dmmptss  5233  cocnvss  5262  fnres  5449  resasplitss  5516  fabexg  5524  f0  5527  ffvresb  5810  isoini2  5960  dmoprabss  6103  elmpocl  6217  elmpom  6403  tposssxp  6415  dftpos4  6429  smores  6458  smores2  6460  iordsmo  6463  swoer  6730  swoord1  6731  swoord2  6732  ecss  6745  ecopovsym  6800  ecopovtrn  6801  ecopover  6802  ecopovsymg  6803  ecopovtrng  6804  ecopoverg  6805  opabfi  7132  sbthlem7  7162  caserel  7286  ctssdccl  7310  pw1on  7444  pinn  7529  niex  7532  ltrelpi  7544  dmaddpi  7545  dmmulpi  7546  enqex  7580  ltrelnq  7585  enq0ex  7659  ltrelpr  7725  enrex  7957  ltrelsr  7958  ltrelre  8053  axaddf  8088  axmulf  8089  ltrelxr  8240  lerelxr  8242  nn0ssre  9406  nn0ssz  9497  rpre  9895  fz1ssfz0  10352  infssuzcldc  10495  swrd00g  11230  cau3  11676  fsum3cvg3  11958  isumshft  12052  explecnv  12067  clim2prod  12101  ntrivcvgap  12110  dvdszrcl  12354  dvdsflip  12413  phimullem  12798  eulerthlemfi  12801  eulerthlemrprm  12802  eulerthlema  12803  eulerthlemh  12804  eulerthlemth  12805  4sqlem1  12962  4sqlem19  12983  ctiunctlemuom  13058  structcnvcnv  13099  fvsetsid  13117  strleun  13188  dmtopon  14749  lmfval  14919  lmbrf  14941  cnconst2  14959  txuni2  14982  xmeter  15162  ivthinclemex  15368  dvidsslem  15419  dvconstss  15424  dvrecap  15439  lgsquadlemofi  15807  lgsquadlem1  15808  lgsquadlem2  15809  2sqlem7  15852