Theorem eqsstrri 3985

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 2774	. 2 ⊢ 𝐴 = 𝐵
3		eqsstr3.2	. 2 ⊢ 𝐵 ⊆ 𝐶
4	2, 3	eqsstri 3984	1 ⊢ 𝐴 ⊆ 𝐶

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ss 3923

This theorem is used by:  3sstr3i  3988  inss2  4190  dmv  5914  idssxp  6053  ofrfvalg  7692  ofval  7695  ofrval  7696  off  7702  ofres  7703  ofco  7709  dftpos4  8247  smores2  8347  dmttrcl  9697  rnttrcl  9698  onwf  9809  r0weon  10012  dju1dif  10172  unctb  10203  infmap2  10216  itunitc  10420  axcclem  10456  dfnn3  12262  cotr2  15038  ressbasssg  17319  ressbasssOLD  17322  prdsle  17537  prdsless  17538  cntrss  19445  dprd2da  20158  opsrle  22248  indiscld  23298  leordtval2  23419  fiuncmp  23611  prdstopn  23836  ustneism  24432  icchmeo  25151  itg1addlem4  25909  itg1addlem5  25910  aannenlem3  26544  efifo  26763  konigsbergssiedgw  30672  pjoml4i  32010  5oai  32084  3oai  32091  bdopssadj  32504  xrge00  33398  xrge0mulc1cn  34395  esumdivc  34537  rpsqrtcn  35045  subfacp1lem5  35713  filnetlem3  36948  filnetlem4  36949  mblfinlem4  38368  itg2gt0cn  38383  psubspset  40576  psubclsetN  40768  dvrelog2  42889  dvrelog3  42890  readvrec2  43180  relexpaddss  44502  corcltrcl  44523  relopabVD  45667  cncfiooicc  46666  amgmwlem  50707