Theorem eqsstri 3224

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

Syntax hints:   = wceq 1372   ⊆ wss 3165

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178

This theorem is referenced by:  eqsstrri  3225  ssrab2  3277  ssrab3  3278  rabssab  3280  difdifdirss  3544  ifssun  3584  opabss  4107  brab2ga  4749  relopabi  4802  dmopabss  4889  resss  4982  relres  4986  exse2  5055  rnin  5091  rnxpss  5113  cnvcnvss  5136  dmmptss  5178  cocnvss  5207  fnres  5391  resasplitss  5454  fabexg  5462  f0  5465  ffvresb  5742  isoini2  5887  dmoprabss  6026  elmpocl  6140  tposssxp  6334  dftpos4  6348  smores  6377  smores2  6379  iordsmo  6382  swoer  6647  swoord1  6648  swoord2  6649  ecss  6662  ecopovsym  6717  ecopovtrn  6718  ecopover  6719  ecopovsymg  6720  ecopovtrng  6721  ecopoverg  6722  opabfi  7034  sbthlem7  7064  caserel  7188  ctssdccl  7212  pw1on  7337  pinn  7421  niex  7424  ltrelpi  7436  dmaddpi  7437  dmmulpi  7438  enqex  7472  ltrelnq  7477  enq0ex  7551  ltrelpr  7617  enrex  7849  ltrelsr  7850  ltrelre  7945  axaddf  7980  axmulf  7981  ltrelxr  8132  lerelxr  8134  nn0ssre  9298  nn0ssz  9389  rpre  9781  fz1ssfz0  10238  infssuzcldc  10376  cau3  11368  fsum3cvg3  11649  isumshft  11743  explecnv  11758  clim2prod  11792  ntrivcvgap  11801  dvdszrcl  12045  dvdsflip  12104  phimullem  12489  eulerthlemfi  12492  eulerthlemrprm  12493  eulerthlema  12494  eulerthlemh  12495  eulerthlemth  12496  4sqlem1  12653  4sqlem19  12674  ctiunctlemuom  12749  structcnvcnv  12790  fvsetsid  12808  strleun  12878  dmtopon  14437  lmfval  14606  lmbrf  14629  cnconst2  14647  txuni2  14670  xmeter  14850  ivthinclemex  15056  dvidsslem  15107  dvconstss  15112  dvrecap  15127  lgsquadlemofi  15495  lgsquadlem1  15496  lgsquadlem2  15497  2sqlem7  15540