Theorem 3sstr4g 4012

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ss 3943

This theorem is referenced by:  rabss2  4053  unss2  4162  sslin  4218  intss  4945  ssopab2  5521  xpss12  5669  coss1  5835  coss2  5836  cnvss  5852  rnss  5919  ssres  5990  ssres2  5991  imass1  6088  imass2  6089  predpredss  6297  predrelss  6326  ssoprab2  7473  ressuppss  8180  tposss  8224  onovuni  8354  ss2ixp  8922  fodomfi  9320  fodomfiOLD  9340  coss12d  14989  isumsplit  15854  isumrpcl  15857  cvgrat  15897  gsumzf1o  19891  gsumzmhm  19916  gsumzinv  19924  fldc  20742  dsmmsubg  21701  qustgpopn  24056  metnrmlem2  24798  ovolsslem  25435  uniioombllem3  25536  ulmres  26347  xrlimcnp  26928  pntlemq  27562  cusgredg  29349  sspba  30654  shlej2i  31306  chpssati  32290  iunrnmptss  32492  mptssALT  32599  pmtrcnelor  33048  rspectopn  33844  zarmxt1  33857  bnj1408  35013  subfacp1lem6  35153  mthmpps  35550  bj-gabss  36899  qsss1  38253  cossss  38389  disjdmqscossss  38767  aomclem4  43028  cotrclrcl  43713  ovnsslelem  46537  isubgredgss  47826  fldcALTV  48255