Theorem 3sstr4g 4026

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3947

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964

This theorem is referenced by:  rabss2  4074  unss2  4180  sslin  4233  intss  4972  ssopab2  5545  xpss12  5690  coss1  5853  coss2  5854  cnvss  5870  rnss  5936  ssres  6006  ssres2  6007  imass1  6097  imass2  6098  predpredss  6304  predrelss  6335  ssoprab2  7473  ressuppss  8164  tposss  8208  onovuni  8338  ss2ixp  8900  fodomfi  9321  coss12d  14915  isumsplit  15782  isumrpcl  15785  cvgrat  15825  gsumzf1o  19774  gsumzmhm  19799  gsumzinv  19807  dsmmsubg  21289  qustgpopn  23615  metnrmlem2  24367  ovolsslem  24992  uniioombllem3  25093  ulmres  25891  xrlimcnp  26462  pntlemq  27093  cusgredg  28670  sspba  29967  shlej2i  30619  chpssati  31603  iunrnmptss  31784  mptssALT  31887  pmtrcnelor  32239  rspectopn  32835  zarmxt1  32848  bnj1408  34035  subfacp1lem6  34164  mthmpps  34561  bj-gabss  35803  qsss1  37145  cossss  37283  disjdmqscossss  37661  aomclem4  41784  cotrclrcl  42478  ovnsslelem  45262  fldc  46934  fldcALTV  46952