Theorem eqsstri 3187

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

Syntax hints:   = wceq 1353   ⊆ wss 3129

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142

This theorem is referenced by:  eqsstrri  3188  ssrab2  3240  ssrab3  3241  rabssab  3243  difdifdirss  3507  ifssun  3548  opabss  4067  brab2ga  4701  relopabi  4752  dmopabss  4839  resss  4931  relres  4935  exse2  5002  rnin  5038  rnxpss  5060  cnvcnvss  5083  dmmptss  5125  cocnvss  5154  fnres  5332  resasplitss  5395  fabexg  5403  f0  5406  ffvresb  5679  isoini2  5819  dmoprabss  5956  elmpocl  6068  tposssxp  6249  dftpos4  6263  smores  6292  smores2  6294  iordsmo  6297  swoer  6562  swoord1  6563  swoord2  6564  ecss  6575  ecopovsym  6630  ecopovtrn  6631  ecopover  6632  ecopovsymg  6633  ecopovtrng  6634  ecopoverg  6635  sbthlem7  6961  caserel  7085  ctssdccl  7109  pw1on  7224  pinn  7307  niex  7310  ltrelpi  7322  dmaddpi  7323  dmmulpi  7324  enqex  7358  ltrelnq  7363  enq0ex  7437  ltrelpr  7503  enrex  7735  ltrelsr  7736  ltrelre  7831  axaddf  7866  axmulf  7867  ltrelxr  8017  lerelxr  8019  nn0ssre  9179  nn0ssz  9270  rpre  9659  fz1ssfz0  10116  cau3  11123  fsum3cvg3  11403  isumshft  11497  explecnv  11512  clim2prod  11546  ntrivcvgap  11555  dvdszrcl  11798  dvdsflip  11856  infssuzcldc  11951  phimullem  12224  eulerthlemfi  12227  eulerthlemrprm  12228  eulerthlema  12229  eulerthlemh  12230  eulerthlemth  12231  4sqlem1  12385  ctiunctlemuom  12436  structcnvcnv  12477  fvsetsid  12495  strleun  12562  dmtopon  13493  lmfval  13662  lmbrf  13685  cnconst2  13703  txuni2  13726  xmeter  13906  ivthinclemex  14090  dvrecap  14147  2sqlem7  14438