Theorem eqsstr3i 3599

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 19-Oct-1999.)

Hypotheses

Ref	Expression
eqsstr3.1	⊢ 𝐵 = 𝐴
eqsstr3.2	⊢ 𝐵 ⊆ 𝐶

Assertion

Ref	Expression
eqsstr3i	⊢ 𝐴 ⊆ 𝐶

Proof of Theorem eqsstr3i

Step	Hyp	Ref	Expression
1		eqsstr3.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	eqcomi 2619	. 2 ⊢ 𝐴 = 𝐵
3		eqsstr3.2	. 2 ⊢ 𝐵 ⊆ 𝐶
4	2, 3	eqsstri 3598	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1475   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  inss2  3796  dmv  5262  ofrfval  6803  ofval  6804  ofrval  6805  off  6810  ofres  6811  ofco  6815  dftpos4  7258  smores2  7338  onwf  8576  r0weon  8718  cda1dif  8881  unctb  8910  infmap2  8923  itunitc  9126  axcclem  9162  dfnn3  10911  bcm1k  12964  bcpasc  12970  cotr2  13564  ressbasss  15759  strlemor1  15796  prdsle  15945  prdsless  15946  dprd2da  18264  opsrle  19296  indiscld  20705  leordtval2  20826  fiuncmp  21017  prdstopn  21241  ustneism  21837  itg1addlem4  23272  itg1addlem5  23273  tdeglem4  23624  aannenlem3  23889  efifo  24097  advlogexp  24201  pjoml4i  27830  5oai  27904  3oai  27911  bdopssadj  28324  xrge00  29017  xrge0mulc1cn  29315  esumdivc  29472  ballotlemodife  29886  subfacp1lem5  30420  filnetlem3  31545  filnetlem4  31546  mblfinlem4  32619  itg2gt0cn  32635  psubspset  34048  psubclsetN  34240  relexpaddss  37029  corcltrcl  37050  relopabVD  38159  cncfiooicc  38780  stoweidlem34  38927  konigsbergssiedgw  41419  amgmwlem  42357