Theorem eqsstrri 3962

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

Syntax hints:   = wceq 1547   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ss 3900

This theorem is referenced by:  3sstr3i  3965  inss2  4166  dmv  5864  idssxp  6001  ofrfvalg  7628  ofval  7631  ofrval  7632  off  7638  ofres  7639  ofco  7645  dftpos4  8185  smores2  8284  dmttrcl  9633  rnttrcl  9634  onwf  9745  r0weon  9925  dju1dif  10086  unctb  10117  infmap2  10130  itunitc  10334  axcclem  10370  dfnn3  12179  cotr2  14930  ressbasssg  17198  ressbasssOLD  17201  prdsle  17416  prdsless  17417  cntrss  19297  dprd2da  20010  opsrle  22023  indiscld  23074  leordtval2  23195  fiuncmp  23387  prdstopn  23611  ustneism  24207  icchmeo  24926  itg1addlem4  25684  itg1addlem5  25685  aannenlem3  26314  efifo  26529  konigsbergssiedgw  30338  pjoml4i  31676  5oai  31750  3oai  31757  bdopssadj  32170  xrge00  33093  xrge0mulc1cn  34125  esumdivc  34267  rpsqrtcn  34777  subfacp1lem5  35412  filnetlem3  36608  filnetlem4  36609  mblfinlem4  38027  itg2gt0cn  38042  psubspset  40236  psubclsetN  40428  dvrelog2  42549  dvrelog3  42550  readvrec2  42838  relexpaddss  44162  corcltrcl  44183  relopabVD  45344  cncfiooicc  46337  amgmwlem  50292