Theorem 3sstr4g 4003

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

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

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 2702

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

This theorem is referenced by:  rabss2  4044  unss2  4153  sslin  4209  intss  4936  ssopab2  5509  xpss12  5656  coss1  5822  coss2  5823  cnvss  5839  rnss  5906  ssres  5977  ssres2  5978  imass1  6075  imass2  6076  predpredss  6284  predrelss  6313  ssoprab2  7460  ressuppss  8165  tposss  8209  onovuni  8314  ss2ixp  8886  fodomfi  9268  fodomfiOLD  9288  coss12d  14945  isumsplit  15813  isumrpcl  15816  cvgrat  15856  gsumzf1o  19849  gsumzmhm  19874  gsumzinv  19882  fldc  20700  dsmmsubg  21659  qustgpopn  24014  metnrmlem2  24756  ovolsslem  25392  uniioombllem3  25493  ulmres  26304  xrlimcnp  26885  pntlemq  27519  cusgredg  29358  sspba  30663  shlej2i  31315  chpssati  32299  iunrnmptss  32501  mptssALT  32606  pmtrcnelor  33055  rspectopn  33864  zarmxt1  33877  bnj1408  35033  subfacp1lem6  35179  mthmpps  35576  bj-gabss  36930  qsss1  38284  cossss  38423  disjdmqscossss  38802  aomclem4  43053  cotrclrcl  43738  ovnsslelem  46565  isubgredgss  47869  fldcALTV  48324