Theorem eqsstri 3274

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

Syntax hints:   = wceq 1398   ⊆ wss 3214

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  eqsstrri  3275  ssrab2  3327  ssrab3  3328  rabssab  3331  difdifdirss  3598  ifssun  3641  opabss  4179  brab2ga  4830  relopabi  4885  dmopabss  4973  resss  5067  relres  5071  exse2  5141  rnin  5177  rnxpss  5199  cnvcnvss  5222  dmmptss  5264  cocnvss  5293  fnres  5480  resasplitss  5549  fabexg  5559  f0  5563  ffvresb  5845  isoini2  5998  dmoprabss  6143  elmpocl  6257  elmpom  6447  tposssxp  6493  dftpos4  6507  smores  6536  smores2  6538  iordsmo  6541  swoer  6808  swoord1  6809  swoord2  6810  ecss  6823  ecopovsym  6878  ecopovtrn  6879  ecopover  6880  ecopovsymg  6881  ecopovtrng  6882  ecopoverg  6883  opabfi  7213  sbthlem7  7246  caserel  7391  ctssdccl  7415  pw1on  7549  pinn  7640  niex  7643  ltrelpi  7655  dmaddpi  7656  dmmulpi  7657  enqex  7691  ltrelnq  7696  enq0ex  7770  ltrelpr  7836  enrex  8068  ltrelsr  8069  ltrelre  8164  axaddf  8199  axmulf  8200  ltrelxr  8350  lerelxr  8352  nn0ssre  9517  nn0ssz  9612  rpre  10011  fz1ssfz0  10473  infssuzcldc  10617  swrd00g  11366  cau3  11825  fsum3cvg3  12107  isumshft  12201  explecnv  12216  clim2prod  12250  ntrivcvgap  12259  dvdszrcl  12503  dvdsflip  12562  phimullem  12947  eulerthlemfi  12950  eulerthlemrprm  12951  eulerthlema  12952  eulerthlemh  12953  eulerthlemth  12954  4sqlem1  13111  4sqlem19  13132  ctiunctlemuom  13271  structcnvcnv  13312  fvsetsid  13330  strleun  13401  dmtopon  15014  lmfval  15184  lmbrf  15206  cnconst2  15224  txuni2  15247  xmeter  15427  ivthinclemex  15633  dvidsslem  15684  dvconstss  15689  dvrecap  15704  lgsquadlemofi  16075  lgsquadlem1  16076  lgsquadlem2  16077  2sqlem7  16120