Theorem eqsstri 3256

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

Syntax hints:   = wceq 1395   ⊆ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  eqsstrri  3257  ssrab2  3309  ssrab3  3310  rabssab  3312  difdifdirss  3576  ifssun  3617  opabss  4148  brab2ga  4794  relopabi  4847  dmopabss  4935  resss  5029  relres  5033  exse2  5102  rnin  5138  rnxpss  5160  cnvcnvss  5183  dmmptss  5225  cocnvss  5254  fnres  5440  resasplitss  5507  fabexg  5515  f0  5518  ffvresb  5800  isoini2  5949  dmoprabss  6092  elmpocl  6206  tposssxp  6401  dftpos4  6415  smores  6444  smores2  6446  iordsmo  6449  swoer  6716  swoord1  6717  swoord2  6718  ecss  6731  ecopovsym  6786  ecopovtrn  6787  ecopover  6788  ecopovsymg  6789  ecopovtrng  6790  ecopoverg  6791  opabfi  7111  sbthlem7  7141  caserel  7265  ctssdccl  7289  pw1on  7422  pinn  7507  niex  7510  ltrelpi  7522  dmaddpi  7523  dmmulpi  7524  enqex  7558  ltrelnq  7563  enq0ex  7637  ltrelpr  7703  enrex  7935  ltrelsr  7936  ltrelre  8031  axaddf  8066  axmulf  8067  ltrelxr  8218  lerelxr  8220  nn0ssre  9384  nn0ssz  9475  rpre  9868  fz1ssfz0  10325  infssuzcldc  10467  swrd00g  11196  cau3  11641  fsum3cvg3  11922  isumshft  12016  explecnv  12031  clim2prod  12065  ntrivcvgap  12074  dvdszrcl  12318  dvdsflip  12377  phimullem  12762  eulerthlemfi  12765  eulerthlemrprm  12766  eulerthlema  12767  eulerthlemh  12768  eulerthlemth  12769  4sqlem1  12926  4sqlem19  12947  ctiunctlemuom  13022  structcnvcnv  13063  fvsetsid  13081  strleun  13152  dmtopon  14712  lmfval  14882  lmbrf  14904  cnconst2  14922  txuni2  14945  xmeter  15125  ivthinclemex  15331  dvidsslem  15382  dvconstss  15387  dvrecap  15402  lgsquadlemofi  15770  lgsquadlem1  15771  lgsquadlem2  15772  2sqlem7  15815