Theorem eqsstri 3280

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

Syntax hints:   = wceq 1402   ⊆ wss 3220

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 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 theorem 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 referenced by:  eqsstrri  3281  ssrab2  3333  ssrab3  3334  rabssab  3337  difdifdirss  3609  ifssun  3652  opabss  4190  brab2ga  4845  relopabi  4900  dmopabss  4988  resss  5082  relres  5086  exse2  5156  rnin  5192  rnxpss  5214  cnvcnvss  5237  dmmptss  5279  cocnvss  5308  fnres  5495  resasplitss  5564  fabexg  5574  f0  5578  ffvresb  5862  isoini2  6015  dmoprabss  6160  elmpocl  6274  elmpom  6464  tposssxp  6510  dftpos4  6524  smores  6553  smores2  6555  iordsmo  6558  swoer  6825  swoord1  6826  swoord2  6827  ecss  6840  ecopovsym  6895  ecopovtrn  6896  ecopover  6897  ecopovsymg  6898  ecopovtrng  6899  ecopoverg  6900  opabfi  7237  sbthlem7  7270  caserel  7417  ctssdccl  7441  pw1on  7575  pinn  7666  niex  7669  ltrelpi  7681  dmaddpi  7682  dmmulpi  7683  enqex  7717  ltrelnq  7722  enq0ex  7796  ltrelpr  7862  enrex  8094  ltrelsr  8095  ltrelre  8190  axaddf  8225  axmulf  8226  ltrelxr  8376  lerelxr  8378  nn0ssre  9546  nn0ssz  9641  rpre  10040  fz1ssfz0  10502  infssuzcldc  10646  swrd00g  11399  cau3  11859  fsum3cvg3  12141  isumshft  12235  explecnv  12250  clim2prod  12284  ntrivcvgap  12293  dvdszrcl  12537  dvdsflip  12596  phimullem  12981  eulerthlemfi  12984  eulerthlemrprm  12985  eulerthlema  12986  eulerthlemh  12987  eulerthlemth  12988  4sqlem1  13145  4sqlem19  13166  ctiunctlemuom  13305  structcnvcnv  13346  fvsetsid  13364  strleun  13435  dmtopon  15047  lmfval  15217  lmbrf  15239  cnconst2  15257  txuni2  15280  xmeter  15460  ivthinclemex  15666  dvidsslem  15717  dvconstss  15722  dvrecap  15737  lgsquadlemofi  16109  lgsquadlem1  16110  lgsquadlem2  16111  2sqlem7  16154