Theorem eqsstri 3156

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

Syntax hints:   = wceq 1332   ⊆ wss 3098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-11 1483  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-ext 2136

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150  df-in 3104  df-ss 3111

This theorem is referenced by:  eqsstrri  3157  ssrab2  3209  rabssab  3211  difdifdirss  3474  ifssun  3515  opabss  4024  brab2ga  4654  relopabi  4705  dmopabss  4791  resss  4883  relres  4887  exse2  4953  rnin  4988  rnxpss  5010  cnvcnvss  5033  dmmptss  5075  cocnvss  5104  fnres  5279  resasplitss  5342  fabexg  5350  f0  5353  ffvresb  5623  isoini2  5760  dmoprabss  5893  elmpocl  6008  tposssxp  6186  dftpos4  6200  smores  6229  smores2  6231  iordsmo  6234  swoer  6497  swoord1  6498  swoord2  6499  ecss  6510  ecopovsym  6565  ecopovtrn  6566  ecopover  6567  ecopovsymg  6568  ecopovtrng  6569  ecopoverg  6570  sbthlem7  6896  caserel  7017  ctssdccl  7041  pw1on  7140  pinn  7208  niex  7211  ltrelpi  7223  dmaddpi  7224  dmmulpi  7225  enqex  7259  ltrelnq  7264  enq0ex  7338  ltrelpr  7404  enrex  7636  ltrelsr  7637  ltrelre  7732  axaddf  7767  axmulf  7768  ltrelxr  7917  lerelxr  7919  nn0ssre  9073  nn0ssz  9164  rpre  9545  fz1ssfz0  9997  cau3  10992  fsum3cvg3  11270  isumshft  11364  explecnv  11379  clim2prod  11413  ntrivcvgap  11422  dvdszrcl  11665  dvdsflip  11716  infssuzcldc  11811  phimullem  12068  ctiunctlemuom  12116  structcnvcnv  12145  fvsetsid  12163  strleun  12218  dmtopon  12360  lmfval  12531  lmbrf  12554  cnconst2  12572  txuni2  12595  xmeter  12775  ivthinclemex  12959  dvrecap  13016