Theorem eqsstri 3216

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

Syntax hints:   = wceq 1364   ⊆ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  eqsstrri  3217  ssrab2  3269  ssrab3  3270  rabssab  3272  difdifdirss  3536  ifssun  3576  opabss  4098  brab2ga  4739  relopabi  4792  dmopabss  4879  resss  4971  relres  4975  exse2  5044  rnin  5080  rnxpss  5102  cnvcnvss  5125  dmmptss  5167  cocnvss  5196  fnres  5377  resasplitss  5440  fabexg  5448  f0  5451  ffvresb  5728  isoini2  5869  dmoprabss  6008  elmpocl  6122  tposssxp  6316  dftpos4  6330  smores  6359  smores2  6361  iordsmo  6364  swoer  6629  swoord1  6630  swoord2  6631  ecss  6644  ecopovsym  6699  ecopovtrn  6700  ecopover  6701  ecopovsymg  6702  ecopovtrng  6703  ecopoverg  6704  opabfi  7008  sbthlem7  7038  caserel  7162  ctssdccl  7186  pw1on  7311  pinn  7395  niex  7398  ltrelpi  7410  dmaddpi  7411  dmmulpi  7412  enqex  7446  ltrelnq  7451  enq0ex  7525  ltrelpr  7591  enrex  7823  ltrelsr  7824  ltrelre  7919  axaddf  7954  axmulf  7955  ltrelxr  8106  lerelxr  8108  nn0ssre  9272  nn0ssz  9363  rpre  9754  fz1ssfz0  10211  infssuzcldc  10344  cau3  11299  fsum3cvg3  11580  isumshft  11674  explecnv  11689  clim2prod  11723  ntrivcvgap  11732  dvdszrcl  11976  dvdsflip  12035  phimullem  12420  eulerthlemfi  12423  eulerthlemrprm  12424  eulerthlema  12425  eulerthlemh  12426  eulerthlemth  12427  4sqlem1  12584  4sqlem19  12605  ctiunctlemuom  12680  structcnvcnv  12721  fvsetsid  12739  strleun  12809  dmtopon  14367  lmfval  14536  lmbrf  14559  cnconst2  14577  txuni2  14600  xmeter  14780  ivthinclemex  14986  dvidsslem  15037  dvconstss  15042  dvrecap  15057  lgsquadlemofi  15425  lgsquadlem1  15426  lgsquadlem2  15427  2sqlem7  15470