Theorem eqsstri 3280

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

This proof depends on syntax axioms:   = wceq 1402   C_ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  eqsstrri  3281  ssrab2  3333  ssrab3  3334  rabssab  3337  difdifdirss  3612  ifssun  3655  opabss  4196  brab2ga  4852  relopabi  4907  dmopabss  4995  resss  5089  relres  5093  exse2  5164  rnin  5200  rnxpss  5222  cnvcnvss  5245  dmmptss  5287  cocnvss  5316  fnres  5503  resasplitss  5572  fabexg  5582  f0  5586  fvopab4ndm  5806  ffvresb  5874  isoini2  6028  dmoprabss  6173  elmpocl  6287  elmpom  6478  tposssxp  6525  dftpos4  6539  smores  6568  smores2  6570  iordsmo  6573  swoer  6840  swoord1  6841  swoord2  6842  ecss  6855  ecopovsym  6910  ecopovtrn  6911  ecopover  6912  ecopovsymg  6913  ecopovtrng  6914  ecopoverg  6915  opabfi  7253  sbthlem7  7287  fdmfifsupp  7301  0fsupp  7305  caserel  7433  ctssdccl  7457  pw1on  7591  pinn  7682  niex  7685  ltrelpi  7697  dmaddpi  7698  dmmulpi  7699  enqex  7733  ltrelnq  7738  enq0ex  7812  ltrelpr  7878  enrex  8110  ltrelsr  8111  ltrelre  8206  axaddf  8241  axmulf  8242  ltrelxr  8392  lerelxr  8394  nn0ssre  9578  nn0ssz  9671  rpre  10077  fz1ssfz0  10540  infssuzcldc  10684  swrd00g  11442  cau3  11903  fsum3cvg3  12187  isumshft  12281  explecnv  12296  clim2prod  12330  ntrivcvgap  12339  dvdszrcl  12583  dvdsflip  12642  phimullem  13031  eulerthlemfi  13034  eulerthlemrprm  13035  eulerthlema  13036  eulerthlemh  13037  eulerthlemth  13038  4sqlem1  13195  4sqlem19  13216  ctiunctlemuom  13384  structcnvcnv  13425  fvsetsid  13443  strleun  13516  cntzsgrpcl  14166  dmtopon  15266  lmfval  15436  lmbrf  15458  cnconst2  15476  txuni2  15499  xmeter  15679  ivthinclemex  15885  dvidsslem  15936  dvconstss  15941  dvrecap  15956  ppiqub  16310  lgsquadlemofi  16417  lgsquadlem1  16418  lgsquadlem2  16419  2sqlem7  16462