Theorem 3sstr4g 3998

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

Syntax hints:   → wi 4   = wceq 1567   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930

This theorem is referenced by:  ss2rabd  4034  rabss2  4039  rabss2OLD  4040  unss2  4148  sslin  4203  intss  4938  ssopab2  5532  xpss12  5677  coss1  5842  coss2  5843  cnvss  5859  rnss  5930  ssres  6003  ssres2  6004  imass1  6104  imass2  6105  predpredss  6310  predrelss  6339  ssoprab2  7479  ressuppss  8179  tposss  8223  onovuni  8329  ss2ixp  8908  fodomfi  9272  coss12d  15009  isumsplit  15894  isumrpcl  15897  cvgrat  15937  gsumzf1o  19982  gsumzmhm  20007  gsumzinv  20015  fldc  20865  dsmmsubg  21862  qustgpopn  24246  metnrmlem2  24987  ovolsslem  25612  uniioombllem3  25713  ulmres  26517  xrlimcnp  27099  pntlemq  27731  cusgredg  29715  sspba  31020  shlej2i  31672  chpssati  32656  iunrnmptss  32851  mptssALT  32960  pmtrcnelor  33352  rspectopn  34202  zarmxt1  34215  bnj1408  35369  subfacp1lem6  35610  mthmpps  36007  bj-gabss  37493  qsss1  38868  cossss  39088  disjdmqscossss  39479  aomclem4  43710  cotrclrcl  44394  ovnsslelem  47200  isubgredgss  48553  fldcALTV  49020