Theorem eqsstr3i 3785

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

Syntax hints:   = wceq 1631   ⊆ wss 3723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-in 3730  df-ss 3737

This theorem is referenced by:  inss2  3982  dmv  5478  ofrfval  7056  ofval  7057  ofrval  7058  off  7063  ofres  7064  ofco  7068  dftpos4  7527  smores2  7608  onwf  8861  r0weon  9039  cda1dif  9204  unctb  9233  infmap2  9246  itunitc  9449  axcclem  9485  dfnn3  11240  cotr2  13926  ressbasss  16139  strlemor1OLD  16177  prdsle  16330  prdsless  16331  dprd2da  18649  opsrle  19690  indiscld  21116  leordtval2  21237  fiuncmp  21428  prdstopn  21652  ustneism  22247  itg1addlem4  23686  itg1addlem5  23687  tdeglem4  24040  aannenlem3  24305  efifo  24514  konigsbergssiedgw  27430  pjoml4i  28786  5oai  28860  3oai  28867  bdopssadj  29280  xrge00  30026  xrge0mulc1cn  30327  esumdivc  30485  rpsqrtcn  31011  subfacp1lem5  31504  filnetlem3  32712  filnetlem4  32713  mblfinlem4  33781  itg2gt0cn  33796  psubspset  35551  psubclsetN  35743  relexpaddss  38534  corcltrcl  38555  relopabVD  39657  cncfiooicc  40620  amgmwlem  43074