Theorem eqsstrrd 3285

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)

Hypotheses

Ref	Expression
eqsstrrd.1	⊢ (𝜑 → 𝐵 = 𝐴)
eqsstrrd.2	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Assertion

Ref	Expression
eqsstrrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem eqsstrrd

Step	Hyp	Ref	Expression
1		eqsstrrd.1	. . 3 ⊢ (𝜑 → 𝐵 = 𝐴)
2	1	eqcomd 2244	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		eqsstrrd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	2, 3	eqsstrd 3284	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1402   ⊆ wss 3220

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  ssxpbm  5218  ssxp1  5219  ssxp2  5220  suppssof1  6310  tfrlemiubacc  6591  tfr1onlemubacc  6607  tfrcllemubacc  6620  oaword1  6734  phplem4dom  7153  fisseneq  7232  nnnninfeq2  7459  archnqq  7774  hashdmprop2dom  11274  imasaddfnlemg  13612  resmhm2  13772  cmnsubm  14089  ringidss  14307  subrg1  14512  subrgdvds  14516  subrguss  14517  subrginv  14518  islss3  14688  lspsnneg  14729  epttop  15114  metequiv2  15520  limccnpcntop  15699  limccnp2lem  15700  limccnp2cntop  15701  umgredgprv  16270  uspgrupgrushgr  16337  usgrumgruspgr  16340  nnsf  16953