Theorem eqsstrri 3994

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 19-Oct-1999.)

Hypotheses

Ref	Expression
eqsstr3.1	⊢ 𝐵 = 𝐴
eqsstr3.2	⊢ 𝐵 ⊆ 𝐶

Assertion

Ref	Expression
eqsstrri	⊢ 𝐴 ⊆ 𝐶

Proof of Theorem eqsstrri

Step	Hyp	Ref	Expression
1		eqsstr3.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	eqcomi 2738	. 2 ⊢ 𝐴 = 𝐵
3		eqsstr3.2	. 2 ⊢ 𝐵 ⊆ 𝐶
4	2, 3	eqsstri 3993	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1540   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931

This theorem is referenced by:  3sstr3i  3997  inss2  4201  dmv  5886  idssxp  6020  ofrfvalg  7661  ofval  7664  ofrval  7665  off  7671  ofres  7672  ofco  7678  dftpos4  8224  smores2  8323  dmttrcl  9674  rnttrcl  9675  onwf  9783  r0weon  9965  dju1dif  10126  unctb  10157  infmap2  10170  itunitc  10374  axcclem  10410  dfnn3  12200  cotr2  14943  ressbasssg  17207  ressbasssOLD  17210  prdsle  17425  prdsless  17426  cntrss  19263  dprd2da  19974  opsrle  21954  indiscld  22978  leordtval2  23099  fiuncmp  23291  prdstopn  23515  ustneism  24111  icchmeo  24838  itg1addlem4  25600  itg1addlem5  25601  aannenlem3  26238  efifo  26456  konigsbergssiedgw  30179  pjoml4i  31516  5oai  31590  3oai  31597  bdopssadj  32010  xrge00  32953  xrge0mulc1cn  33931  esumdivc  34073  rpsqrtcn  34584  subfacp1lem5  35171  filnetlem3  36368  filnetlem4  36369  mblfinlem4  37654  itg2gt0cn  37669  psubspset  39738  psubclsetN  39930  dvrelog2  42052  dvrelog3  42053  readvrec2  42349  relexpaddss  43707  corcltrcl  43728  relopabVD  44890  cncfiooicc  45892  amgmwlem  49791