Theorem eqsstri 3259

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

Syntax hints:   = wceq 1397   ⊆ 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  10496  swrd00g  11234  cau3  11693  fsum3cvg3  11975  isumshft  12069  explecnv  12084  clim2prod  12118  ntrivcvgap  12127  dvdszrcl  12371  dvdsflip  12430  phimullem  12815  eulerthlemfi  12818  eulerthlemrprm  12819  eulerthlema  12820  eulerthlemh  12821  eulerthlemth  12822  4sqlem1  12979  4sqlem19  13000  ctiunctlemuom  13075  structcnvcnv  13116  fvsetsid  13134  strleun  13205  dmtopon  14766  lmfval  14936  lmbrf  14958  cnconst2  14976  txuni2  14999  xmeter  15179  ivthinclemex  15385  dvidsslem  15436  dvconstss  15441  dvrecap  15456  lgsquadlemofi  15824  lgsquadlem1  15825  lgsquadlem2  15826  2sqlem7  15869