Theorem eqsstrri 3956

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

This proof depends on syntax axioms:   = wceq 1569   ⊆ wss 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3897

This theorem is used by:  3sstr3i  3959  inss2  4133  dmv  5904  idssxp  6042  ofrfvalg  7703  ofval  7706  ofrval  7707  off  7713  ofres  7714  ofco  7720  dftpos4  8267  smores2  8367  dmttrcl  9727  rnttrcl  9728  onwf  9845  r0weon  10096  dju1dif  10256  unctb  10287  infmap2  10300  itunitc  10504  axcclem  10540  dfnn3  12354  cotr2  15137  ressbasssg  17422  ressbasssOLD  17425  prdsle  17640  prdsless  17641  cntrss  19552  dprd2da  20265  opsrle  22363  indiscld  23416  leordtval2  23537  fiuncmp  23729  prdstopn  23954  ustneism  24550  icchmeo  25269  itg1addlem4  26027  itg1addlem5  26028  aannenlem3  26664  efifo  26882  konigsbergssiedgw  30858  pjoml4i  32196  5oai  32270  3oai  32277  bdopssadj  32690  xrge00  33623  xrge0mulc1cn  34621  esumdivc  34763  rpsqrtcn  35270  j0ltalephlem  35948  subfacp1lem5  36037  filnetlem3  37262  filnetlem4  37263  mblfinlem4  38685  itg2gt0cn  38700  psubspset  40908  psubclsetN  41100  dvrelog2  43221  dvrelog3  43222  readvrec2  43519  relexpaddss  44825  corcltrcl  44846  relopabVD  45990  cncfiooicc  47011  amgmwlem  51169