Theorem 3sstr4g 3920

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3399  df-in 3848  df-ss 3858

This theorem is referenced by:  rabss2  3965  unss2  4069  sslin  4123  intss  4854  ssopab2  5398  xpss12  5534  coss1  5692  coss2  5693  cnvss  5709  rnss  5776  ssres  5846  ssres2  5847  imass1  5932  imass2  5933  predpredss  6129  ssoprab2  7230  ressuppss  7871  tposss  7915  onovuni  8001  ss2ixp  8513  fodomfi  8863  coss12d  14414  isumsplit  15281  isumrpcl  15284  cvgrat  15324  gsumzf1o  19144  gsumzmhm  19169  gsumzinv  19177  dsmmsubg  20552  qustgpopn  22864  metnrmlem2  23605  ovolsslem  24229  uniioombllem3  24330  ulmres  25127  xrlimcnp  25698  pntlemq  26329  cusgredg  27358  sspba  28654  shlej2i  29306  chpssati  30290  iunrnmptss  30471  mptssALT  30579  pmtrcnelor  30929  rspectopn  31381  zarmxt1  31394  bnj1408  32579  subfacp1lem6  32710  mthmpps  33107  qsss1  36035  cossss  36160  aomclem4  40438  cotrclrcl  40880  fldc  45159  fldcALTV  45177