Theorem eqsstri 3260

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

Syntax hints:   = wceq 1398   ⊆ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  eqsstrri  3261  ssrab2  3313  ssrab3  3314  rabssab  3317  difdifdirss  3581  ifssun  3624  opabss  4158  brab2ga  4807  relopabi  4861  dmopabss  4949  resss  5043  relres  5047  exse2  5117  rnin  5153  rnxpss  5175  cnvcnvss  5198  dmmptss  5240  cocnvss  5269  fnres  5456  resasplitss  5524  fabexg  5532  f0  5536  ffvresb  5818  isoini2  5970  dmoprabss  6113  elmpocl  6227  elmpom  6412  tposssxp  6458  dftpos4  6472  smores  6501  smores2  6503  iordsmo  6506  swoer  6773  swoord1  6774  swoord2  6775  ecss  6788  ecopovsym  6843  ecopovtrn  6844  ecopover  6845  ecopovsymg  6846  ecopovtrng  6847  ecopoverg  6848  opabfi  7175  sbthlem7  7205  caserel  7329  ctssdccl  7353  pw1on  7487  pinn  7572  niex  7575  ltrelpi  7587  dmaddpi  7588  dmmulpi  7589  enqex  7623  ltrelnq  7628  enq0ex  7702  ltrelpr  7768  enrex  8000  ltrelsr  8001  ltrelre  8096  axaddf  8131  axmulf  8132  ltrelxr  8282  lerelxr  8284  nn0ssre  9448  nn0ssz  9541  rpre  9939  fz1ssfz0  10397  infssuzcldc  10541  swrd00g  11279  cau3  11738  fsum3cvg3  12020  isumshft  12114  explecnv  12129  clim2prod  12163  ntrivcvgap  12172  dvdszrcl  12416  dvdsflip  12475  phimullem  12860  eulerthlemfi  12863  eulerthlemrprm  12864  eulerthlema  12865  eulerthlemh  12866  eulerthlemth  12867  4sqlem1  13024  4sqlem19  13045  ctiunctlemuom  13120  structcnvcnv  13161  fvsetsid  13179  strleun  13250  dmtopon  14817  lmfval  14987  lmbrf  15009  cnconst2  15027  txuni2  15050  xmeter  15230  ivthinclemex  15436  dvidsslem  15487  dvconstss  15492  dvrecap  15507  lgsquadlemofi  15878  lgsquadlem1  15879  lgsquadlem2  15880  2sqlem7  15923