Theorem 3sstr4g 4054

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  rabss2  4101  unss2  4210  sslin  4264  intss  4993  ssopab2  5565  xpss12  5715  coss1  5880  coss2  5881  cnvss  5897  rnss  5964  ssres  6033  ssres2  6034  imass1  6131  imass2  6132  predpredss  6339  predrelss  6369  ssoprab2  7518  ressuppss  8224  tposss  8268  onovuni  8398  ss2ixp  8968  fodomfi  9378  fodomfiOLD  9398  coss12d  15021  isumsplit  15888  isumrpcl  15891  cvgrat  15931  gsumzf1o  19954  gsumzmhm  19979  gsumzinv  19987  fldc  20807  dsmmsubg  21786  qustgpopn  24149  metnrmlem2  24901  ovolsslem  25538  uniioombllem3  25639  ulmres  26449  xrlimcnp  27029  pntlemq  27663  cusgredg  29459  sspba  30759  shlej2i  31411  chpssati  32395  iunrnmptss  32588  mptssALT  32693  pmtrcnelor  33084  rspectopn  33813  zarmxt1  33826  bnj1408  35012  subfacp1lem6  35153  mthmpps  35550  bj-gabss  36901  qsss1  38245  cossss  38381  disjdmqscossss  38759  aomclem4  43014  cotrclrcl  43704  ovnsslelem  46481  uspgrimprop  47757  fldcALTV  48055