Theorem eqsstrri 4002

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

Syntax hints:   = wceq 1537   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  inss2  4206  dmv  5792  idssxp  5916  ofrfval  7417  ofval  7418  ofrval  7419  off  7424  ofres  7425  ofco  7429  dftpos4  7911  smores2  7991  onwf  9259  r0weon  9438  dju1dif  9598  unctb  9627  infmap2  9640  itunitc  9843  axcclem  9879  dfnn3  11652  cotr2  14337  ressbasss  16556  prdsle  16735  prdsless  16736  cntrss  18460  dprd2da  19164  opsrle  20256  indiscld  21699  leordtval2  21820  fiuncmp  22012  prdstopn  22236  ustneism  22832  itg1addlem4  24300  itg1addlem5  24301  tdeglem4  24654  aannenlem3  24919  efifo  25131  konigsbergssiedgw  28029  pjoml4i  29364  5oai  29438  3oai  29445  bdopssadj  29858  xrge00  30673  xrge0mulc1cn  31184  esumdivc  31342  rpsqrtcn  31864  subfacp1lem5  32431  filnetlem3  33728  filnetlem4  33729  mblfinlem4  34947  itg2gt0cn  34962  psubspset  36895  psubclsetN  37087  relexpaddss  40112  corcltrcl  40133  relopabVD  41284  cncfiooicc  42226  amgmwlem  44952