Theorem 3sstr4g 3787

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

Syntax hints:   → wi 4   = wceq 1632   ⊆ wss 3715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-in 3722  df-ss 3729

This theorem is referenced by:  rabss2  3826  unss2  3927  sslin  3982  intss  4650  ssopab2  5151  xpss12  5281  coss1  5433  coss2  5434  cnvss  5450  rnss  5509  ssres  5582  ssres2  5583  imass1  5658  imass2  5659  predpredss  5847  ssoprab2  6876  ressuppss  7482  tposss  7522  onovuni  7608  ss2ixp  8087  fodomfi  8404  coss12d  13912  isumsplit  14771  isumrpcl  14774  cvgrat  14814  gsumzf1o  18513  gsumzmhm  18537  gsumzinv  18545  dsmmsubg  20289  qustgpopn  22124  metnrmlem2  22864  ovolsslem  23452  uniioombllem3  23553  ulmres  24341  xrlimcnp  24894  pntlemq  25489  cusgredg  26530  sspba  27891  shlej2i  28547  chpssati  29531  mptssALT  29783  bnj1408  31411  subfacp1lem6  31474  mthmpps  31786  qsss1  34377  cossss  34503  aomclem4  38129  cotrclrcl  38536  fldc  42593  fldcALTV  42611