Theorem 3sstr4g 4027

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

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

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 3955  df-ss 3965

This theorem is referenced by:  rabss2  4075  unss2  4181  sslin  4234  intss  4973  ssopab2  5546  xpss12  5691  coss1  5855  coss2  5856  cnvss  5872  rnss  5938  ssres  6008  ssres2  6009  imass1  6100  imass2  6101  predpredss  6307  predrelss  6338  ssoprab2  7479  ressuppss  8170  tposss  8214  onovuni  8344  ss2ixp  8906  fodomfi  9327  coss12d  14923  isumsplit  15790  isumrpcl  15793  cvgrat  15833  gsumzf1o  19821  gsumzmhm  19846  gsumzinv  19854  dsmmsubg  21517  qustgpopn  23844  metnrmlem2  24596  ovolsslem  25225  uniioombllem3  25326  ulmres  26124  xrlimcnp  26697  pntlemq  27328  cusgredg  28936  sspba  30235  shlej2i  30887  chpssati  31871  iunrnmptss  32052  mptssALT  32155  pmtrcnelor  32510  rspectopn  33133  zarmxt1  33146  bnj1408  34333  subfacp1lem6  34462  mthmpps  34859  bj-gabss  36118  qsss1  37460  cossss  37598  disjdmqscossss  37976  aomclem4  42101  cotrclrcl  42795  ovnsslelem  45575  fldc  47070  fldcALTV  47088