Theorem 3sstr4g 3976

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 3961	. 2 ⊢ (𝜑 → 𝐶 ⊆ 𝐵)
4		3sstr4g.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	sseqtrrdi 3964	1 ⊢ (𝜑 → 𝐶 ⊆ 𝐷)

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  ss2rabd  4013  rabss2  4018  rabss2OLD  4019  unss2  4128  sslin  4184  intss  4912  ssopab2  5496  xpss12  5641  coss1  5806  coss2  5807  cnvss  5823  rnss  5890  ssres  5964  ssres2  5965  imass1  6062  imass2  6063  predpredss  6268  predrelss  6297  ssoprab2  7430  ressuppss  8128  tposss  8172  onovuni  8277  ss2ixp  8853  fodomfi  9217  fodomfiOLD  9235  coss12d  14929  isumsplit  15800  isumrpcl  15803  cvgrat  15843  gsumzf1o  19882  gsumzmhm  19907  gsumzinv  19915  fldc  20756  dsmmsubg  21737  qustgpopn  24099  metnrmlem2  24840  ovolsslem  25465  uniioombllem3  25566  ulmres  26370  xrlimcnp  26949  pntlemq  27582  cusgredg  29511  sspba  30817  shlej2i  31469  chpssati  32453  iunrnmptss  32654  mptssALT  32766  pmtrcnelor  33171  rspectopn  34031  zarmxt1  34044  bnj1408  35198  subfacp1lem6  35387  mthmpps  35784  bj-gabss  37262  qsss1  38634  cossss  38854  disjdmqscossss  39245  aomclem4  43507  cotrclrcl  44191  ovnsslelem  47010  isubgredgss  48357  fldcALTV  48824