Theorem 3sstr4g 3962

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  rabss2  4007  unss2  4111  sslin  4165  intss  4897  ssopab2  5452  xpss12  5595  coss1  5753  coss2  5754  cnvss  5770  rnss  5837  ssres  5907  ssres2  5908  imass1  5998  imass2  5999  predpredss  6198  ssoprab2  7321  ressuppss  7970  tposss  8014  onovuni  8144  ss2ixp  8656  fodomfi  9022  coss12d  14611  isumsplit  15480  isumrpcl  15483  cvgrat  15523  gsumzf1o  19428  gsumzmhm  19453  gsumzinv  19461  dsmmsubg  20860  qustgpopn  23179  metnrmlem2  23929  ovolsslem  24553  uniioombllem3  24654  ulmres  25452  xrlimcnp  26023  pntlemq  26654  cusgredg  27694  sspba  28990  shlej2i  29642  chpssati  30626  iunrnmptss  30806  mptssALT  30914  pmtrcnelor  31262  rspectopn  31719  zarmxt1  31732  bnj1408  32916  subfacp1lem6  33047  mthmpps  33444  bj-gabss  35050  qsss1  36350  cossss  36475  aomclem4  40798  cotrclrcl  41239  fldc  45529  fldcALTV  45547