Theorem eqsstr3d 2148

Description: Substitution of equality into a subclass relationship.

Hypotheses

Ref	Expression
eqsstr3d.1	⊢ (φ → B = A)
eqsstr3d.2	⊢ (φ → B ⊆ C)

Assertion

Ref	Expression
eqsstr3d	⊢ (φ → A ⊆ C)

Proof of Theorem eqsstr3d

Step	Hyp	Ref	Expression
1		eqsstr3d.1	. . 3 ⊢ (φ → B = A)
2	1	eqcomd 1523	. 2 ⊢ (φ → A = B)
3		eqsstr3d.2	. 2 ⊢ (φ → B ⊆ C)
4	2, 3	eqsstrd 2147	1 ⊢ (φ → A ⊆ C)

Syntax hints:   → wi 3   = wceq 992   ⊆ wss 2099

This theorem is referenced by:  sspr 2540  ssxpb 3560  oaword1 4322  omword2 4341  r1val1 4804  rankxpl 4856  rankxplim3 4860  basgen2 7851  caussi 8165  sspg 8641  ssps 8643  sspn 8649  kbass5 10333  mdslj1i 10527  mdslj2i 10528  sh1dle 10559  shatomistici 10569  sumdmdii 10624  fictb 11423  cldregopn 11468  cnntr 11474  cptclsscpt 11489  cnpfillim 11686  elfilmap 11690  fmf 11693  fmbas 11694  fmfnfm 11704  ufcomp 11734  tosdir 11755  filnetlem4 11766

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-in 2103  df-ss 2105

Copyright terms: Public domain