Theorem 3sstr4g 3960

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 3945	. 2 ⊢ (𝐶 ⊆ 𝐷 ↔ 𝐴 ⊆ 𝐵)
5	1, 4	sylibr 237	1 ⊢ (𝜑 → 𝐶 ⊆ 𝐷)

Syntax hints:   → wi 4   = wceq 1538   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  rabss2  4005  unss2  4108  sslin  4161  intss  4859  ssopab2  5398  xpss12  5534  coss1  5690  coss2  5691  cnvss  5707  rnss  5773  ssres  5845  ssres2  5846  imass1  5931  imass2  5932  predpredss  6122  ssoprab2  7201  ressuppss  7832  tposss  7876  onovuni  7962  ss2ixp  8457  fodomfi  8781  coss12d  14323  isumsplit  15187  isumrpcl  15190  cvgrat  15231  gsumzf1o  19025  gsumzmhm  19050  gsumzinv  19058  dsmmsubg  20432  qustgpopn  22725  metnrmlem2  23465  ovolsslem  24088  uniioombllem3  24189  ulmres  24983  xrlimcnp  25554  pntlemq  26185  cusgredg  27214  sspba  28510  shlej2i  29162  chpssati  30146  iunrnmptss  30329  mptssALT  30438  pmtrcnelor  30785  rspectopn  31220  zarmxt1  31233  bnj1408  32418  subfacp1lem6  32545  mthmpps  32942  qsss1  35705  cossss  35830  aomclem4  40001  cotrclrcl  40443  fldc  44707  fldcALTV  44725