Theorem eqsstri 3173

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

Syntax hints:   = wceq 1343   ⊆ wss 3115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-in 3121  df-ss 3128

This theorem is referenced by:  eqsstrri  3174  ssrab2  3226  ssrab3  3227  rabssab  3229  difdifdirss  3492  ifssun  3533  opabss  4045  brab2ga  4678  relopabi  4729  dmopabss  4815  resss  4907  relres  4911  exse2  4977  rnin  5012  rnxpss  5034  cnvcnvss  5057  dmmptss  5099  cocnvss  5128  fnres  5303  resasplitss  5366  fabexg  5374  f0  5377  ffvresb  5647  isoini2  5786  dmoprabss  5920  elmpocl  6035  tposssxp  6213  dftpos4  6227  smores  6256  smores2  6258  iordsmo  6261  swoer  6525  swoord1  6526  swoord2  6527  ecss  6538  ecopovsym  6593  ecopovtrn  6594  ecopover  6595  ecopovsymg  6596  ecopovtrng  6597  ecopoverg  6598  sbthlem7  6924  caserel  7048  ctssdccl  7072  pw1on  7178  pinn  7246  niex  7249  ltrelpi  7261  dmaddpi  7262  dmmulpi  7263  enqex  7297  ltrelnq  7302  enq0ex  7376  ltrelpr  7442  enrex  7674  ltrelsr  7675  ltrelre  7770  axaddf  7805  axmulf  7806  ltrelxr  7955  lerelxr  7957  nn0ssre  9114  nn0ssz  9205  rpre  9592  fz1ssfz0  10048  cau3  11053  fsum3cvg3  11333  isumshft  11427  explecnv  11442  clim2prod  11476  ntrivcvgap  11485  dvdszrcl  11728  dvdsflip  11785  infssuzcldc  11880  phimullem  12153  eulerthlemfi  12156  eulerthlemrprm  12157  eulerthlema  12158  eulerthlemh  12159  eulerthlemth  12160  4sqlem1  12314  ctiunctlemuom  12365  structcnvcnv  12406  fvsetsid  12424  strleun  12479  dmtopon  12621  lmfval  12792  lmbrf  12815  cnconst2  12833  txuni2  12856  xmeter  13036  ivthinclemex  13220  dvrecap  13277  2sqlem7  13557