Theorem 3sstr4g 4040

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.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		3sstr4g.2	. . 3 ⊢ 𝐶 = 𝐴
3		3sstr4g.3	. . 3 ⊢ 𝐷 = 𝐵
4	2, 3	sseq12i 4025	. 2 ⊢ (𝐶 ⊆ 𝐷 ↔ 𝐴 ⊆ 𝐵)
5	1, 4	sylibr 234	1 ⊢ (𝜑 → 𝐶 ⊆ 𝐷)

Syntax hints:   → wi 4   = wceq 1536   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979

This theorem is referenced by:  rabss2  4087  unss2  4196  sslin  4250  intss  4973  ssopab2  5555  xpss12  5703  coss1  5868  coss2  5869  cnvss  5885  rnss  5952  ssres  6023  ssres2  6024  imass1  6121  imass2  6122  predpredss  6329  predrelss  6359  ssoprab2  7500  ressuppss  8206  tposss  8250  onovuni  8380  ss2ixp  8948  fodomfi  9347  fodomfiOLD  9367  coss12d  15007  isumsplit  15872  isumrpcl  15875  cvgrat  15915  gsumzf1o  19944  gsumzmhm  19969  gsumzinv  19977  fldc  20801  dsmmsubg  21780  qustgpopn  24143  metnrmlem2  24895  ovolsslem  25532  uniioombllem3  25633  ulmres  26445  xrlimcnp  27025  pntlemq  27659  cusgredg  29455  sspba  30755  shlej2i  31407  chpssati  32391  iunrnmptss  32585  mptssALT  32691  pmtrcnelor  33093  rspectopn  33827  zarmxt1  33840  bnj1408  35028  subfacp1lem6  35169  mthmpps  35566  bj-gabss  36917  qsss1  38270  cossss  38406  disjdmqscossss  38784  aomclem4  43045  cotrclrcl  43731  ovnsslelem  46515  isubgredgss  47788  uspgrimprop  47810  fldcALTV  48175