Theorem eqsstrri 4031

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

Syntax hints:   = wceq 1537   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ss 3980

This theorem is referenced by:  inss2  4246  dmv  5936  idssxp  6069  ofrfvalg  7705  ofval  7708  ofrval  7709  off  7715  ofres  7716  ofco  7722  dftpos4  8269  smores2  8393  dmttrcl  9759  rnttrcl  9760  onwf  9868  r0weon  10050  dju1dif  10211  unctb  10242  infmap2  10255  itunitc  10459  axcclem  10495  dfnn3  12278  cotr2  15013  ressbasssg  17282  ressbasssOLD  17285  prdsle  17509  prdsless  17510  cntrss  19362  dprd2da  20077  opsrle  22083  indiscld  23115  leordtval2  23236  fiuncmp  23428  prdstopn  23652  ustneism  24248  icchmeo  24985  itg1addlem4  25748  itg1addlem4OLD  25749  itg1addlem5  25750  aannenlem3  26387  efifo  26604  konigsbergssiedgw  30279  pjoml4i  31616  5oai  31690  3oai  31697  bdopssadj  32110  xrge00  33000  xrge0mulc1cn  33902  esumdivc  34064  rpsqrtcn  34587  subfacp1lem5  35169  filnetlem3  36363  filnetlem4  36364  mblfinlem4  37647  itg2gt0cn  37662  psubspset  39727  psubclsetN  39919  dvrelog2  42046  dvrelog3  42047  readvrec2  42370  relexpaddss  43708  corcltrcl  43729  relopabVD  44899  cncfiooicc  45850  amgmwlem  49033