Theorem eqsstri 3185

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

Syntax hints:   = wceq 1353   ⊆ wss 3127

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-11 1504  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-in 3133  df-ss 3140

This theorem is referenced by:  eqsstrri  3186  ssrab2  3238  ssrab3  3239  rabssab  3241  difdifdirss  3505  ifssun  3546  opabss  4062  brab2ga  4695  relopabi  4746  dmopabss  4832  resss  4924  relres  4928  exse2  4995  rnin  5030  rnxpss  5052  cnvcnvss  5075  dmmptss  5117  cocnvss  5146  fnres  5324  resasplitss  5387  fabexg  5395  f0  5398  ffvresb  5671  isoini2  5810  dmoprabss  5947  elmpocl  6059  tposssxp  6240  dftpos4  6254  smores  6283  smores2  6285  iordsmo  6288  swoer  6553  swoord1  6554  swoord2  6555  ecss  6566  ecopovsym  6621  ecopovtrn  6622  ecopover  6623  ecopovsymg  6624  ecopovtrng  6625  ecopoverg  6626  sbthlem7  6952  caserel  7076  ctssdccl  7100  pw1on  7215  pinn  7283  niex  7286  ltrelpi  7298  dmaddpi  7299  dmmulpi  7300  enqex  7334  ltrelnq  7339  enq0ex  7413  ltrelpr  7479  enrex  7711  ltrelsr  7712  ltrelre  7807  axaddf  7842  axmulf  7843  ltrelxr  7992  lerelxr  7994  nn0ssre  9151  nn0ssz  9242  rpre  9629  fz1ssfz0  10085  cau3  11090  fsum3cvg3  11370  isumshft  11464  explecnv  11479  clim2prod  11513  ntrivcvgap  11522  dvdszrcl  11765  dvdsflip  11822  infssuzcldc  11917  phimullem  12190  eulerthlemfi  12193  eulerthlemrprm  12194  eulerthlema  12195  eulerthlemh  12196  eulerthlemth  12197  4sqlem1  12351  ctiunctlemuom  12402  structcnvcnv  12443  fvsetsid  12461  strleun  12518  dmtopon  13090  lmfval  13261  lmbrf  13284  cnconst2  13302  txuni2  13325  xmeter  13505  ivthinclemex  13689  dvrecap  13746  2sqlem7  14026