Theorem 3sstr4g 3966

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  rabss2  4011  unss2  4115  sslin  4168  intss  4900  ssopab2  5459  xpss12  5604  coss1  5764  coss2  5765  cnvss  5781  rnss  5848  ssres  5918  ssres2  5919  imass1  6009  imass2  6010  predpredss  6209  predrelss  6240  ssoprab2  7343  ressuppss  7999  tposss  8043  onovuni  8173  ss2ixp  8698  fodomfi  9092  coss12d  14683  isumsplit  15552  isumrpcl  15555  cvgrat  15595  gsumzf1o  19513  gsumzmhm  19538  gsumzinv  19546  dsmmsubg  20950  qustgpopn  23271  metnrmlem2  24023  ovolsslem  24648  uniioombllem3  24749  ulmres  25547  xrlimcnp  26118  pntlemq  26749  cusgredg  27791  sspba  29089  shlej2i  29741  chpssati  30725  iunrnmptss  30905  mptssALT  31012  pmtrcnelor  31360  rspectopn  31817  zarmxt1  31830  bnj1408  33016  subfacp1lem6  33147  mthmpps  33544  bj-gabss  35123  qsss1  36423  cossss  36548  aomclem4  40882  cotrclrcl  41350  fldc  45641  fldcALTV  45659