Theorem eqsstr3i 3830

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

Syntax hints:   = wceq 1653   ⊆ wss 3767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-in 3774  df-ss 3781

This theorem is referenced by:  inss2  4027  dmv  5542  idssxp  5671  ofrfval  7137  ofval  7138  ofrval  7139  off  7144  ofres  7145  ofco  7149  dftpos4  7607  smores2  7688  onwf  8941  r0weon  9119  cda1dif  9284  unctb  9313  infmap2  9326  itunitc  9529  axcclem  9565  dfnn3  11326  cotr2  14056  ressbasss  16254  prdsle  16434  prdsless  16435  dprd2da  18754  opsrle  19795  indiscld  21221  leordtval2  21342  fiuncmp  21533  prdstopn  21757  ustneism  22352  itg1addlem4  23804  itg1addlem5  23805  tdeglem4  24158  aannenlem3  24423  efifo  24632  konigsbergssiedgw  27589  pjoml4i  28963  5oai  29037  3oai  29044  bdopssadj  29457  xrge00  30194  xrge0mulc1cn  30495  esumdivc  30653  rpsqrtcn  31183  subfacp1lem5  31675  filnetlem3  32879  filnetlem4  32880  mblfinlem4  33930  itg2gt0cn  33945  psubspset  35757  psubclsetN  35949  relexpaddss  38781  corcltrcl  38802  relopabVD  39885  cncfiooicc  40839  amgmwlem  43338