Theorem eqsstri 3045

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 3039	. 2 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)
4	1, 3	mpbir 144	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1287   ⊆ wss 2988

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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-11 1440  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-in 2994  df-ss 3001

This theorem is referenced by:  eqsstr3i  3046  ssrab2  3095  rabssab  3097  difdifdirss  3354  opabss  3877  brab2ga  4481  relopabi  4531  dmopabss  4616  resss  4704  relres  4708  exse2  4773  rnin  4807  rnxpss  4828  cnvcnvss  4851  dmmptss  4893  cocnvss  4922  fnres  5095  resasplitss  5153  fabexg  5161  f0  5164  ffvresb  5424  isoini2  5559  dmoprabss  5687  elmpt2cl  5799  tposssxp  5968  dftpos4  5982  smores  6011  smores2  6013  iordsmo  6016  swoer  6272  swoord1  6273  swoord2  6274  ecss  6285  ecopovsym  6340  ecopovtrn  6341  ecopover  6342  ecopovsymg  6343  ecopovtrng  6344  ecopoverg  6345  sbthlem7  6616  djuun  6704  caserel  6722  pinn  6812  niex  6815  ltrelpi  6827  dmaddpi  6828  dmmulpi  6829  enqex  6863  ltrelnq  6868  enq0ex  6942  ltrelpr  7008  enrex  7227  ltrelsr  7228  ltrelre  7314  ltrelxr  7491  lerelxr  7493  nn0ssre  8610  nn0ssz  8701  rpre  9072  cau3  10444  fisumcvg3  10676  dvdszrcl  10683  dvdsflip  10734  infssuzcldc  10829  phimullem  11083