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

Syntax hints:   = wceq 1540   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968

This theorem is referenced by:  3sstr3i  4034  inss2  4238  dmv  5933  idssxp  6067  ofrfvalg  7705  ofval  7708  ofrval  7709  off  7715  ofres  7716  ofco  7722  dftpos4  8270  smores2  8394  dmttrcl  9761  rnttrcl  9762  onwf  9870  r0weon  10052  dju1dif  10213  unctb  10244  infmap2  10257  itunitc  10461  axcclem  10497  dfnn3  12280  cotr2  15016  ressbasssg  17282  ressbasssOLD  17285  prdsle  17507  prdsless  17508  cntrss  19349  dprd2da  20062  opsrle  22065  indiscld  23099  leordtval2  23220  fiuncmp  23412  prdstopn  23636  ustneism  24232  icchmeo  24971  itg1addlem4  25734  itg1addlem5  25735  aannenlem3  26372  efifo  26589  konigsbergssiedgw  30269  pjoml4i  31606  5oai  31680  3oai  31687  bdopssadj  32100  xrge00  33017  xrge0mulc1cn  33940  esumdivc  34084  rpsqrtcn  34608  subfacp1lem5  35189  filnetlem3  36381  filnetlem4  36382  mblfinlem4  37667  itg2gt0cn  37682  psubspset  39746  psubclsetN  39938  dvrelog2  42065  dvrelog3  42066  readvrec2  42391  relexpaddss  43731  corcltrcl  43752  relopabVD  44921  cncfiooicc  45909  amgmwlem  49321