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  5959  dmoprabss  6102  elmpocl  6216  elmpom  6402  tposssxp  6414  dftpos4  6428  smores  6457  smores2  6459  iordsmo  6462  swoer  6729  swoord1  6730  swoord2  6731  ecss  6744  ecopovsym  6799  ecopovtrn  6800  ecopover  6801  ecopovsymg  6802  ecopovtrng  6803  ecopoverg  6804  opabfi  7131  sbthlem7  7161  caserel  7285  ctssdccl  7309  pw1on  7443  pinn  7528  niex  7531  ltrelpi  7543  dmaddpi  7544  dmmulpi  7545  enqex  7579  ltrelnq  7584  enq0ex  7658  ltrelpr  7724  enrex  7956  ltrelsr  7957  ltrelre  8052  axaddf  8087  axmulf  8088  ltrelxr  8239  lerelxr  8241  nn0ssre  9405  nn0ssz  9496  rpre  9894  fz1ssfz0  10351  infssuzcldc  10494  swrd00g  11229  cau3  11675  fsum3cvg3  11956  isumshft  12050  explecnv  12065  clim2prod  12099  ntrivcvgap  12108  dvdszrcl  12352  dvdsflip  12411  phimullem  12796  eulerthlemfi  12799  eulerthlemrprm  12800  eulerthlema  12801  eulerthlemh  12802  eulerthlemth  12803  4sqlem1  12960  4sqlem19  12981  ctiunctlemuom  13056  structcnvcnv  13097  fvsetsid  13115  strleun  13186  dmtopon  14746  lmfval  14916  lmbrf  14938  cnconst2  14956  txuni2  14979  xmeter  15159  ivthinclemex  15365  dvidsslem  15416  dvconstss  15421  dvrecap  15436  lgsquadlemofi  15804  lgsquadlem1  15805  lgsquadlem2  15806  2sqlem7  15849