Theorem 3sstr4g 3989

Description: Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)

Hypotheses

Ref	Expression
3sstr4g.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
3sstr4g.2	⊢ 𝐶 = 𝐴
3sstr4g.3	⊢ 𝐷 = 𝐵

Assertion

Ref	Expression
3sstr4g	⊢ (𝜑 → 𝐶 ⊆ 𝐷)

Proof of Theorem 3sstr4g

Step	Hyp	Ref	Expression
1		3sstr4g.2	. . 3 ⊢ 𝐶 = 𝐴
2		3sstr4g.1	. . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
3	1, 2	eqsstrid 3974	. 2 ⊢ (𝜑 → 𝐶 ⊆ 𝐵)
4		3sstr4g.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	sseqtrrdi 3977	1 ⊢ (𝜑 → 𝐶 ⊆ 𝐷)

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3903

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  rabss2  4029  unss2  4138  sslin  4194  intss  4919  ssopab2  5489  xpss12  5634  coss1  5798  coss2  5799  cnvss  5815  rnss  5881  ssres  5954  ssres2  5955  imass1  6052  imass2  6053  predpredss  6256  predrelss  6285  ssoprab2  7417  ressuppss  8116  tposss  8160  onovuni  8265  ss2ixp  8837  fodomfi  9201  fodomfiOLD  9220  coss12d  14879  isumsplit  15747  isumrpcl  15750  cvgrat  15790  gsumzf1o  19791  gsumzmhm  19816  gsumzinv  19824  fldc  20669  dsmmsubg  21650  qustgpopn  24005  metnrmlem2  24747  ovolsslem  25383  uniioombllem3  25484  ulmres  26295  xrlimcnp  26876  pntlemq  27510  cusgredg  29369  sspba  30671  shlej2i  31323  chpssati  32307  iunrnmptss  32509  mptssALT  32619  pmtrcnelor  33034  rspectopn  33840  zarmxt1  33853  bnj1408  35009  subfacp1lem6  35168  mthmpps  35565  bj-gabss  36919  qsss1  38273  cossss  38412  disjdmqscossss  38791  aomclem4  43040  cotrclrcl  43725  ovnsslelem  46551  isubgredgss  47859  fldcALTV  48326