Theorem eqsstri 3257

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

Syntax hints:   = wceq 1395   ⊆ wss 3198

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  eqsstrri  3258  ssrab2  3310  ssrab3  3311  rabssab  3313  difdifdirss  3577  ifssun  3618  opabss  4151  brab2ga  4799  relopabi  4853  dmopabss  4941  resss  5035  relres  5039  exse2  5108  rnin  5144  rnxpss  5166  cnvcnvss  5189  dmmptss  5231  cocnvss  5260  fnres  5446  resasplitss  5513  fabexg  5521  f0  5524  ffvresb  5806  isoini2  5955  dmoprabss  6098  elmpocl  6212  elmpom  6398  tposssxp  6410  dftpos4  6424  smores  6453  smores2  6455  iordsmo  6458  swoer  6725  swoord1  6726  swoord2  6727  ecss  6740  ecopovsym  6795  ecopovtrn  6796  ecopover  6797  ecopovsymg  6798  ecopovtrng  6799  ecopoverg  6800  opabfi  7123  sbthlem7  7153  caserel  7277  ctssdccl  7301  pw1on  7434  pinn  7519  niex  7522  ltrelpi  7534  dmaddpi  7535  dmmulpi  7536  enqex  7570  ltrelnq  7575  enq0ex  7649  ltrelpr  7715  enrex  7947  ltrelsr  7948  ltrelre  8043  axaddf  8078  axmulf  8079  ltrelxr  8230  lerelxr  8232  nn0ssre  9396  nn0ssz  9487  rpre  9885  fz1ssfz0  10342  infssuzcldc  10485  swrd00g  11220  cau3  11666  fsum3cvg3  11947  isumshft  12041  explecnv  12056  clim2prod  12090  ntrivcvgap  12099  dvdszrcl  12343  dvdsflip  12402  phimullem  12787  eulerthlemfi  12790  eulerthlemrprm  12791  eulerthlema  12792  eulerthlemh  12793  eulerthlemth  12794  4sqlem1  12951  4sqlem19  12972  ctiunctlemuom  13047  structcnvcnv  13088  fvsetsid  13106  strleun  13177  dmtopon  14737  lmfval  14907  lmbrf  14929  cnconst2  14947  txuni2  14970  xmeter  15150  ivthinclemex  15356  dvidsslem  15407  dvconstss  15412  dvrecap  15427  lgsquadlemofi  15795  lgsquadlem1  15796  lgsquadlem2  15797  2sqlem7  15840