Theorem eqsstrri 3997

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

Syntax hints:   = wceq 1540   ⊆ wss 3917

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 2702

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

This theorem is referenced by:  3sstr3i  4000  inss2  4204  dmv  5889  idssxp  6023  ofrfvalg  7664  ofval  7667  ofrval  7668  off  7674  ofres  7675  ofco  7681  dftpos4  8227  smores2  8326  dmttrcl  9681  rnttrcl  9682  onwf  9790  r0weon  9972  dju1dif  10133  unctb  10164  infmap2  10177  itunitc  10381  axcclem  10417  dfnn3  12207  cotr2  14950  ressbasssg  17214  ressbasssOLD  17217  prdsle  17432  prdsless  17433  cntrss  19270  dprd2da  19981  opsrle  21961  indiscld  22985  leordtval2  23106  fiuncmp  23298  prdstopn  23522  ustneism  24118  icchmeo  24845  itg1addlem4  25607  itg1addlem5  25608  aannenlem3  26245  efifo  26463  konigsbergssiedgw  30186  pjoml4i  31523  5oai  31597  3oai  31604  bdopssadj  32017  xrge00  32960  xrge0mulc1cn  33938  esumdivc  34080  rpsqrtcn  34591  subfacp1lem5  35178  filnetlem3  36375  filnetlem4  36376  mblfinlem4  37661  itg2gt0cn  37676  psubspset  39745  psubclsetN  39937  dvrelog2  42059  dvrelog3  42060  readvrec2  42356  relexpaddss  43714  corcltrcl  43735  relopabVD  44897  cncfiooicc  45899  amgmwlem  49795