Theorem eqsstrri 4044

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

Syntax hints:   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  inss2  4259  dmv  5947  idssxp  6078  ofrfvalg  7722  ofval  7725  ofrval  7726  off  7732  ofres  7733  ofco  7738  dftpos4  8286  smores2  8410  dmttrcl  9790  rnttrcl  9791  onwf  9899  r0weon  10081  dju1dif  10242  unctb  10273  infmap2  10286  itunitc  10490  axcclem  10526  dfnn3  12307  cotr2  15026  ressbasssg  17295  ressbasssOLD  17298  prdsle  17522  prdsless  17523  cntrss  19371  dprd2da  20086  opsrle  22088  indiscld  23120  leordtval2  23241  fiuncmp  23433  prdstopn  23657  ustneism  24253  icchmeo  24990  itg1addlem4  25753  itg1addlem4OLD  25754  itg1addlem5  25755  aannenlem3  26390  efifo  26607  konigsbergssiedgw  30282  pjoml4i  31619  5oai  31693  3oai  31700  bdopssadj  32113  xrge00  32998  xrge0mulc1cn  33887  esumdivc  34047  rpsqrtcn  34570  subfacp1lem5  35152  filnetlem3  36346  filnetlem4  36347  mblfinlem4  37620  itg2gt0cn  37635  psubspset  39701  psubclsetN  39893  dvrelog2  42021  dvrelog3  42022  relexpaddss  43680  corcltrcl  43701  relopabVD  44872  cncfiooicc  45815  amgmwlem  48896