Theorem sseqtrrd 3276

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

Hypotheses

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

Assertion

Ref	Expression
sseqtrrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sseqtrrd

Step	Hyp	Ref	Expression
1		sseqtrrd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sseqtrrd.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2238	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	sseqtrd 3275	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1398   ⊆ wss 3210

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3216  df-ss 3223

This theorem is referenced by:  sseqtrrid  3288  fnfvima  5920  tfrlemiubacc  6560  tfr1onlemubacc  6576  tfrcllemubacc  6589  rdgivallem  6611  nnnninf  7416  nninfwlpoimlemg  7465  ccatass  11292  swrdval2  11339  dfphi2  12913  ctinf  13173  imasaddfnlemg  13519  imasaddvallemg  13520  subsubm  13688  subsubg  13906  subsubrng  14351  subsubrg  14382  lidlss  14616  toponss  14883  ssntr  14979  iscnp3  15060  cnprcl2k  15063  tgcn  15065  tgcnp  15066  ssidcn  15067  cncnp  15087  txcnp  15128  imasnopn  15156  hmeontr  15170  blssec  15295  blssopn  15342  xmettx  15367  metcnp  15369  plyaddlem1  15604  plymullem1  15605  plycoeid3  15614  nnsf  16775  nninfsellemsuc  16782