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  4748  relopabi  4801  dmopabss  4888  resss  4980  relres  4984  exse2  5053  rnin  5089  rnxpss  5111  cnvcnvss  5134  dmmptss  5176  cocnvss  5205  fnres  5386  resasplitss  5449  fabexg  5457  f0  5460  ffvresb  5737  isoini2  5878  dmoprabss  6017  elmpocl  6131  tposssxp  6325  dftpos4  6339  smores  6368  smores2  6370  iordsmo  6373  swoer  6638  swoord1  6639  swoord2  6640  ecss  6653  ecopovsym  6708  ecopovtrn  6709  ecopover  6710  ecopovsymg  6711  ecopovtrng  6712  ecopoverg  6713  opabfi  7017  sbthlem7  7047  caserel  7171  ctssdccl  7195  pw1on  7320  pinn  7404  niex  7407  ltrelpi  7419  dmaddpi  7420  dmmulpi  7421  enqex  7455  ltrelnq  7460  enq0ex  7534  ltrelpr  7600  enrex  7832  ltrelsr  7833  ltrelre  7928  axaddf  7963  axmulf  7964  ltrelxr  8115  lerelxr  8117  nn0ssre  9281  nn0ssz  9372  rpre  9764  fz1ssfz0  10221  infssuzcldc  10359  cau3  11345  fsum3cvg3  11626  isumshft  11720  explecnv  11735  clim2prod  11769  ntrivcvgap  11778  dvdszrcl  12022  dvdsflip  12081  phimullem  12466  eulerthlemfi  12469  eulerthlemrprm  12470  eulerthlema  12471  eulerthlemh  12472  eulerthlemth  12473  4sqlem1  12630  4sqlem19  12651  ctiunctlemuom  12726  structcnvcnv  12767  fvsetsid  12785  strleun  12855  dmtopon  14413  lmfval  14582  lmbrf  14605  cnconst2  14623  txuni2  14646  xmeter  14826  ivthinclemex  15032  dvidsslem  15083  dvconstss  15088  dvrecap  15103  lgsquadlemofi  15471  lgsquadlem1  15472  lgsquadlem2  15473  2sqlem7  15516