Theorem eqsstri 3029

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.)

Hypotheses

Ref	Expression
eqsstr.1	⊢ 𝐴 = 𝐵
eqsstr.2	⊢ 𝐵 ⊆ 𝐶

Assertion

Ref	Expression
eqsstri	⊢ 𝐴 ⊆ 𝐶

Proof of Theorem eqsstri

Step	Hyp	Ref	Expression
1		eqsstr.2	. 2 ⊢ 𝐵 ⊆ 𝐶
2		eqsstr.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	sseq1i 3023	. 2 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)
4	1, 3	mpbir 144	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1284   ⊆ wss 2973

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-11 1437  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-in 2979  df-ss 2986

This theorem is referenced by:  eqsstr3i  3030  ssrab2  3079  rabssab  3081  difdifdirss  3327  opabss  3842  brab2ga  4433  relopabi  4481  dmopabss  4565  resss  4653  relres  4657  exse2  4719  rnin  4753  rnxpss  4774  cnvcnvss  4795  dmmptss  4837  fnres  5035  resasplitss  5089  fabexg  5097  f0  5100  ffvresb  5349  isoini2  5478  dmoprabss  5606  elmpt2cl  5718  tposssxp  5887  dftpos4  5901  smores  5930  smores2  5932  iordsmo  5935  swoer  6157  swoord1  6158  swoord2  6159  ecss  6170  ecopovsym  6225  ecopovtrn  6226  ecopover  6227  ecopovsymg  6228  ecopovtrng  6229  ecopoverg  6230  pinn  6499  niex  6502  ltrelpi  6514  dmaddpi  6515  dmmulpi  6516  enqex  6550  ltrelnq  6555  enq0ex  6629  ltrelpr  6695  enrex  6914  ltrelsr  6915  ltrelre  7001  ltrelxr  7173  lerelxr  7175  nn0ssre  8292  nn0ssz  8369  rpre  8740  cau3  10001  dvdszrcl  10200  dvdsflip  10251  infssuzcldc  10347