Theorem eqsstri 3270

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

Syntax hints:   = wceq 1398   ⊆ wss 3211

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 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224

This theorem is referenced by:  eqsstrri  3271  ssrab2  3323  ssrab3  3324  rabssab  3327  difdifdirss  3594  ifssun  3637  opabss  4174  brab2ga  4825  relopabi  4880  dmopabss  4968  resss  5062  relres  5066  exse2  5136  rnin  5172  rnxpss  5194  cnvcnvss  5217  dmmptss  5259  cocnvss  5288  fnres  5475  resasplitss  5544  fabexg  5554  f0  5558  ffvresb  5840  isoini2  5992  dmoprabss  6135  elmpocl  6249  elmpom  6434  tposssxp  6480  dftpos4  6494  smores  6523  smores2  6525  iordsmo  6528  swoer  6795  swoord1  6796  swoord2  6797  ecss  6810  ecopovsym  6865  ecopovtrn  6866  ecopover  6867  ecopovsymg  6868  ecopovtrng  6869  ecopoverg  6870  opabfi  7200  sbthlem7  7233  caserel  7378  ctssdccl  7402  pw1on  7536  pinn  7624  niex  7627  ltrelpi  7639  dmaddpi  7640  dmmulpi  7641  enqex  7675  ltrelnq  7680  enq0ex  7754  ltrelpr  7820  enrex  8052  ltrelsr  8053  ltrelre  8148  axaddf  8183  axmulf  8184  ltrelxr  8334  lerelxr  8336  nn0ssre  9500  nn0ssz  9595  rpre  9993  fz1ssfz0  10451  infssuzcldc  10595  swrd00g  11341  cau3  11800  fsum3cvg3  12082  isumshft  12176  explecnv  12191  clim2prod  12225  ntrivcvgap  12234  dvdszrcl  12478  dvdsflip  12537  phimullem  12922  eulerthlemfi  12925  eulerthlemrprm  12926  eulerthlema  12927  eulerthlemh  12928  eulerthlemth  12929  4sqlem1  13086  4sqlem19  13107  ctiunctlemuom  13187  structcnvcnv  13228  fvsetsid  13246  strleun  13317  dmtopon  14888  lmfval  15058  lmbrf  15080  cnconst2  15098  txuni2  15121  xmeter  15301  ivthinclemex  15507  dvidsslem  15558  dvconstss  15563  dvrecap  15578  lgsquadlemofi  15949  lgsquadlem1  15950  lgsquadlem2  15951  2sqlem7  15994