Theorem sseqtr4i 3060

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 4-Apr-1995.)

Hypotheses

Ref	Expression
sseqtr4.1	⊢ 𝐴 ⊆ 𝐵
sseqtr4.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
sseqtr4i	⊢ 𝐴 ⊆ 𝐶

Proof of Theorem sseqtr4i

Step	Hyp	Ref	Expression
1		sseqtr4.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		sseqtr4.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2093	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	sseqtri 3059	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1290   ⊆ wss 3000

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-11 1443  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-in 3006  df-ss 3013

This theorem is referenced by:  eqimss2i  3082  difdif2ss  3257  snsspr1  3591  snsspr2  3592  snsstp1  3593  snsstp2  3594  snsstp3  3595  prsstp12  3596  prsstp13  3597  prsstp23  3598  iunxdif2  3784  pwpwssunieq  3823  sssucid  4251  opabssxp  4525  dmresi  4780  cnvimass  4808  ssrnres  4886  cnvcnv  4896  cnvssrndm  4965  dmmpt2ssx  5983  tfrcllemssrecs  6131  sucinc  6220  mapex  6425  exmidpw  6678  casefun  6830  djufun  6839  ressxr  7585  ltrelxr  7601  nnssnn0  8730  un0addcl  8760  un0mulcl  8761  nn0ssxnn0  8793  fzssnn  9536  fzossnn0  9640  isumclim3  10871  isprm3  11432  phimullem  11533  tgvalex  11804