Theorem eqsstri 3280

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

This proof depends on syntax axioms:   = wceq 1402   ⊆ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  eqsstrri  3281  ssrab2  3333  ssrab3  3334  rabssab  3337  difdifdirss  3612  ifssun  3655  opabss  4195  brab2ga  4850  relopabi  4905  dmopabss  4993  resss  5087  relres  5091  exse2  5161  rnin  5197  rnxpss  5219  cnvcnvss  5242  dmmptss  5284  cocnvss  5313  fnres  5500  resasplitss  5569  fabexg  5579  f0  5583  fvopab4ndm  5803  ffvresb  5871  isoini2  6025  dmoprabss  6170  elmpocl  6284  elmpom  6474  tposssxp  6520  dftpos4  6534  smores  6563  smores2  6565  iordsmo  6568  swoer  6835  swoord1  6836  swoord2  6837  ecss  6850  ecopovsym  6905  ecopovtrn  6906  ecopover  6907  ecopovsymg  6908  ecopovtrng  6909  ecopoverg  6910  opabfi  7247  sbthlem7  7280  caserel  7427  ctssdccl  7451  pw1on  7585  pinn  7676  niex  7679  ltrelpi  7691  dmaddpi  7692  dmmulpi  7693  enqex  7727  ltrelnq  7732  enq0ex  7806  ltrelpr  7872  enrex  8104  ltrelsr  8105  ltrelre  8200  axaddf  8235  axmulf  8236  ltrelxr  8386  lerelxr  8388  nn0ssre  9567  nn0ssz  9662  rpre  10061  fz1ssfz0  10524  infssuzcldc  10668  swrd00g  11421  cau3  11881  fsum3cvg3  12163  isumshft  12257  explecnv  12272  clim2prod  12306  ntrivcvgap  12315  dvdszrcl  12559  dvdsflip  12618  phimullem  13003  eulerthlemfi  13006  eulerthlemrprm  13007  eulerthlema  13008  eulerthlemh  13009  eulerthlemth  13010  4sqlem1  13167  4sqlem19  13188  ctiunctlemuom  13327  structcnvcnv  13368  fvsetsid  13386  strleun  13458  dmtopon  15124  lmfval  15294  lmbrf  15316  cnconst2  15334  txuni2  15357  xmeter  15537  ivthinclemex  15743  dvidsslem  15794  dvconstss  15799  dvrecap  15814  lgsquadlemofi  16195  lgsquadlem1  16196  lgsquadlem2  16197  2sqlem7  16240