Theorem 3sstr4g 4011

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

Syntax hints:   → wi 4   = wceq 1533   ⊆ wss 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951

This theorem is referenced by:  rabss2  4053  unss2  4156  sslin  4210  intss  4896  ssopab2  5432  xpss12  5569  coss1  5725  coss2  5726  cnvss  5742  rnss  5808  ssres  5879  ssres2  5880  imass1  5963  imass2  5964  predpredss  6153  ssoprab2  7221  ressuppss  7848  tposss  7892  onovuni  7978  ss2ixp  8473  fodomfi  8796  coss12d  14331  isumsplit  15194  isumrpcl  15197  cvgrat  15238  gsumzf1o  19031  gsumzmhm  19056  gsumzinv  19064  dsmmsubg  20886  qustgpopn  22727  metnrmlem2  23467  ovolsslem  24084  uniioombllem3  24185  ulmres  24975  xrlimcnp  25545  pntlemq  26176  cusgredg  27205  sspba  28503  shlej2i  29155  chpssati  30139  iunrnmptss  30316  mptssALT  30419  pmtrcnelor  30735  bnj1408  32308  subfacp1lem6  32432  mthmpps  32829  qsss1  35544  cossss  35669  aomclem4  39655  cotrclrcl  40085  fldc  44353  fldcALTV  44371