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  11397  fsum3cvg3  11678  isumshft  11772  explecnv  11787  clim2prod  11821  ntrivcvgap  11830  dvdszrcl  12074  dvdsflip  12133  phimullem  12518  eulerthlemfi  12521  eulerthlemrprm  12522  eulerthlema  12523  eulerthlemh  12524  eulerthlemth  12525  4sqlem1  12682  4sqlem19  12703  ctiunctlemuom  12778  structcnvcnv  12819  fvsetsid  12837  strleun  12907  dmtopon  14466  lmfval  14635  lmbrf  14658  cnconst2  14676  txuni2  14699  xmeter  14879  ivthinclemex  15085  dvidsslem  15136  dvconstss  15141  dvrecap  15156  lgsquadlemofi  15524  lgsquadlem1  15525  lgsquadlem2  15526  2sqlem7  15569